:: Translations in Affine Planes
::  by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received June 12, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies DIRAF, SUBSET_1, VECTSP_1, ANALOAF, FUNCT_2, STRUCT_0, TRANSGEO,
      FUNCT_1, AFF_2, INCSP_1, AFF_1, RELAT_1;
 notations PARTFUN1, FUNCT_2, STRUCT_0, ANALOAF, DIRAF, AFF_1, AFF_2, TRANSGEO;
 constructors RELAT_2, PARTFUN1, AFF_1, AFF_2, TRANSGEO, RELSET_1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0;
 requirements SUBSET, BOOLE;
 theorems FUNCT_2, TRANSGEO, AFF_1, AFF_2, FUNCT_1, DIRAF, RELAT_1;
 schemes TRANSGEO;

begin

reserve AS for AffinSpace,
  a,b,c,d,p,q,r,s,x for Element of AS;

definition
  let AS;
  attr AS is Fanoian means
  :Def1:
  for a,b,c,d st a,b // c,d & a,c // b,d & a,d // b,c holds LIN a,b,c;
end;

Lm1: LIN a,b,c & a<>b & a<>c & b<>c & not LIN a,b,p implies ex x st LIN p,a,x
& p<>x & a<>x
proof
  assume that
A1: LIN a,b,c and
A2: a<>b and
A3: a<>c and
A4: b<>c and
A5: not LIN a,b,p;
  a,b // a,c by A1,AFF_1:def 1;
  then b,a // a,c by AFF_1:4;
  then consider x such that
A6: p,a // a,x and
A7: p,b // c,x by A2,DIRAF:40;
A8: now
    assume p = x;
    then p,b // p,c by A7,AFF_1:4;
    then LIN p,b,c by AFF_1:def 1;
    then
A9: LIN b,c,p by AFF_1:6;
    LIN b,c,a & LIN b,c,b by A1,AFF_1:6,7;
    hence contradiction by A4,A5,A9,AFF_1:8;
  end;
A10: now
    assume a = x;
    then
A11: p,b // a,c by A7,AFF_1:4;
    a,b // a,c by A1,AFF_1:def 1;
    then a,b // p,b by A3,A11,AFF_1:5;
    then b,a // b,p by AFF_1:4;
    then LIN b,a,p by AFF_1:def 1;
    hence contradiction by A5,AFF_1:6;
  end;
  a,p // a,x by A6,AFF_1:4;
  then LIN a,p,x by AFF_1:def 1;
  then LIN p,a,x by AFF_1:6;
  hence thesis by A8,A10;
end;

Lm2: LIN a,b,c & a<>b & a<>c & b<>c & not LIN a,b,p & LIN a,b,q implies ex x
st LIN p,q,x & p<>x & q<>x
proof
  assume that
A1: LIN a,b,c and
A2: a<>b and
A3: a<>c and
A4: b<>c and
A5: not LIN a,b,p and
A6: LIN a,b,q;
A7: now
    assume that
A8: q = c and
    q<>a and
    q<>b;
A9: now
      assume
A10:  LIN q,a,p;
      LIN c,a,b & LIN c,a,a by A1,AFF_1:6,7;
      hence contradiction by A3,A5,A8,A10,AFF_1:8;
    end;
    LIN q,a,b by A6,AFF_1:6;
    hence thesis by A2,A3,A4,A8,A9,Lm1;
  end;
A11: now
    assume that
A12: q<>a and
A13: q<>b and
    q<>c;
A14: now
      assume LIN q,a,p;
      then LIN a,q,p by AFF_1:6;
      then
A15:  a,q // a,p by AFF_1:def 1;
      LIN a,q,b by A6,AFF_1:6;
      then a,q // a,b by AFF_1:def 1;
      then a,b // a,p by A12,A15,AFF_1:5;
      hence contradiction by A5,AFF_1:def 1;
    end;
    LIN q,a,b by A6,AFF_1:6;
    hence thesis by A2,A12,A13,A14,Lm1;
  end;
  now
    assume that
A16: q = b and
    q<>a and
    q<>c;
    LIN q,a,c & not LIN q,a,p by A1,A5,A16,AFF_1:6;
    hence thesis by A2,A3,A4,A16,Lm1;
  end;
  hence thesis by A1,A2,A3,A4,A5,A7,A11,Lm1;
end;

Lm3: LIN a,b,c & a<>b & a<>c & b<>c & not LIN a,b,p & p,q // a,b implies ex x
st LIN p,q,x & p<>x & q<>x
proof
  assume that
A1: LIN a,b,c and
A2: a<>b and
A3: a<>c and
A4: b<>c and
A5: not LIN a,b,p and
A6: p,q // a,b;
A7: b<>q
  proof
    assume b = q;
    then b,p // b,a by A6,AFF_1:4;
    then LIN b,p,a by AFF_1:def 1;
    hence contradiction by A5,AFF_1:6;
  end;
A8: a<>q
  proof
    assume a = q;
    then a,p // a,b by A6,AFF_1:4;
    then LIN a,p,b by AFF_1:def 1;
    hence contradiction by A5,AFF_1:6;
  end;
A9: not LIN a,b,q
  proof
    assume
A10: LIN a,b,q;
    then a,b // a,q by AFF_1:def 1;
    then p,q // a,q by A2,A6,AFF_1:5;
    then q,p // q,a by AFF_1:4;
    then LIN q,p,a by AFF_1:def 1;
    then
A11: LIN q,a,p by AFF_1:6;
A12: LIN q,a,a by AFF_1:7;
    LIN q,a,b by A10,AFF_1:6;
    hence contradiction by A5,A8,A11,A12,AFF_1:8;
  end;
  consider r such that
A13: b,c // q,r and
A14: b,q // c,r by DIRAF:40;
  LIN b,a,c by A1,AFF_1:6;
  then b,a // b,c by AFF_1:def 1;
  then b,a // q,r by A4,A13,AFF_1:5;
  then a,b // q,r by AFF_1:4;
  then p,q // q,r by A2,A6,AFF_1:5;
  then q,p // q,r by AFF_1:4;
  then LIN q,p,r by AFF_1:def 1;
  then
A15: LIN p,q,r by AFF_1:6;
A16: not LIN a,c,p
  proof
    assume
A17: LIN a,c,p;
    LIN a,c,b & LIN a,c,a by A1,AFF_1:6,7;
    hence contradiction by A3,A5,A17,AFF_1:8;
  end;
A18: now
    consider s such that
A19: b,a // q,s and
A20: b,q // a,s by DIRAF:40;
A21: q<>s
    proof
      assume q = s;
      then q,b // q,a by A20,AFF_1:4;
      then LIN q,b,a by AFF_1:def 1;
      hence contradiction by A9,AFF_1:6;
    end;
    assume
A22: p = r;
A23: now
      assume p = s;
      then a,p // c,p by A7,A14,A22,A20,AFF_1:5;
      then p,a // p,c by AFF_1:4;
      then LIN p,a,c by AFF_1:def 1;
      hence contradiction by A16,AFF_1:6;
    end;
    a,b // q,s by A19,AFF_1:4;
    then p,q // q,s by A2,A6,AFF_1:5;
    then q,p // q,s by AFF_1:4;
    then LIN q,p,s by AFF_1:def 1;
    then LIN p,q,s by AFF_1:6;
    hence thesis by A23,A21;
  end;
  q<>r
  proof
    assume q = r;
    then q,b // q,c by A14,AFF_1:4;
    then LIN q,b,c by AFF_1:def 1;
    then
A24: LIN b,c,q by AFF_1:6;
    LIN b,c,a & LIN b,c,b by A1,AFF_1:6,7;
    hence contradiction by A4,A9,A24,AFF_1:8;
  end;
  hence thesis by A15,A18;
end;

theorem Th1:
  (ex a,b,c st LIN a,b,c & a<>b & a<>c & b<>c) implies for p,q
  holds ex r st LIN p,q,r & p<>r & q<>r
proof
  given a,b,c such that
A1: LIN a,b,c and
A2: a<>b and
A3: a<>c and
A4: b<>c;
  let p,q;
A5: now
    assume that
A6: LIN a,b,p and
A7: LIN a,b,q;
A8: LIN a,b,b by AFF_1:7;
A9: LIN a,b,a by AFF_1:7;
    now
      assume
A10:  p = c or q = c;
      now
        assume p <> a or q <> b;
A11:    now
          assume that
A12:      p = c and
A13:      p<>a;
          q = b implies thesis by A1,A2,A9,A8,A12,A13,AFF_1:8;
          hence thesis by A1,A2,A4,A7,A8,A12,AFF_1:8;
        end;
        now
          assume that
A14:      q = c and
          q<>b;
          p = b implies thesis by A1,A2,A3,A9,A8,A14,AFF_1:8;
          hence thesis by A1,A2,A4,A6,A8,A14,AFF_1:8;
        end;
        hence thesis by A3,A4,A10,A11;
      end;
      hence thesis by A1,A3,A4;
    end;
    hence thesis by A1,A2,A6,A7,AFF_1:8;
  end;
A15: now
    assume that
A16: not LIN a,b,p and
    not LIN a,b,q;
    now
      consider p9 being Element of AS such that
A17:  a,b // p,p9 and
A18:  p<>p9 by DIRAF:40;
      assume
A19:  not p,q // a,b;
A20:  not LIN p,p9,q
      proof
        assume LIN p,p9,q;
        then p,p9 // p,q by AFF_1:def 1;
        hence contradiction by A19,A17,A18,AFF_1:5;
      end;
      p,p9 // a,b by A17,AFF_1:4;
      then
      ex p99 being Element of AS st LIN p,p9,p99 & p<>p99 & p9<>p99 by A1,A2,A3
,A4,A16,Lm3;
      then consider r such that
A21:  LIN q,p,r and
A22:  q<>r & p<>r by A18,A20,Lm1;
      LIN p,q,r by A21,AFF_1:6;
      hence thesis by A22;
    end;
    hence thesis by A1,A2,A3,A4,A16,Lm3;
  end;
  now
    assume ( not LIN a,b,q)& LIN a,b,p;
    then consider x such that
A23: LIN q,p,x and
A24: q<>x & p<>x by A1,A2,A3,A4,Lm2;
    LIN p,q,x by A23,AFF_1:6;
    hence thesis by A24;
  end;
  hence thesis by A1,A2,A3,A4,A5,A15,Lm2;
end;

reserve AFP for AffinPlane,
  a,a9,b,b9,c,c9,d,p,p9,q,q9,r,x,x9,y,y9,z for Element of AFP,
  A,C,P for Subset of AFP,
  f,g,h,f1,f2 for Permutation of the carrier of AFP;

theorem Th2:
  AFP is Fanoian & a,b // c,d & a,c // b,d & not LIN a,b,c implies
  ex p st LIN b,c,p & LIN a,d,p
proof
  assume ( for a,b,c,d st a,b // c,d & a,c // b,d & a,d // b,c holds LIN a,b,
  c)& a,b // c,d & a,c // b,d & not LIN a,b,c;
  then not a,d // b,c;
  then ex p st LIN a,d,p & LIN b,c,p by AFF_1:60;
  hence thesis;
end;

Lm4: not LIN a,b,x & a,b // x,y & x<>y implies not LIN x,y,a & not LIN b,a,y &
not LIN y,x,b
proof
  assume that
A1: not LIN a,b,x and
A2: a,b // x,y and
A3: x<>y;
  thus not LIN x,y,a
  proof
A4: LIN x,y,x by AFF_1:7;
    assume
A5: LIN x,y,a;
    x,y // a,b by A2,AFF_1:4;
    then LIN x,y,b by A3,A5,AFF_1:9;
    hence contradiction by A1,A3,A5,A4,AFF_1:8;
  end;
  thus not LIN b,a,y
  proof
    assume
A6: LIN b,a,y;
    b,a // y,x & b<>a by A1,A2,AFF_1:4,7;
    then LIN b,a,x by A6,AFF_1:9;
    hence contradiction by A1,AFF_1:6;
  end;
  thus not LIN y,x,b
  proof
A7: LIN y,x,x by AFF_1:7;
    assume
A8: LIN y,x,b;
    y,x // b,a by A2,AFF_1:4;
    then LIN y,x,a by A3,A8,AFF_1:9;
    hence contradiction by A1,A3,A8,A7,AFF_1:8;
  end;
end;

Lm5: not LIN a,b,x & a,b // x,y & a,x // b,y implies not LIN x,y,a & not LIN b
,a,y & not LIN y,x,b
proof
  assume that
A1: not LIN a,b,x and
A2: a,b // x,y and
A3: a,x // b,y;
  x<>y
  proof
    assume x=y;
    then x,a // x,b by A3,AFF_1:4;
    then LIN x,a,b by AFF_1:def 1;
    hence contradiction by A1,AFF_1:6;
  end;
  hence thesis by A1,A2,Lm4;
end;

theorem Th3:
  f is translation & not LIN a,f.a,x & a,f.a // x,y & a,x // f.a,y
  implies y=f.x
proof
  assume
A1: f is translation;
  then
A2: f is dilatation by TRANSGEO:def 11;
  then
A3: a,x // f.a,f.x by TRANSGEO:64;
  assume
A4: ( not LIN a,f.a,x)& a,f.a // x,y & a,x // f.a,y;
  a,f.a // x,f.x by A1,A2,TRANSGEO:78;
  hence thesis by A4,A3,TRANSGEO:76;
end;

theorem Th4:
  AFP is translational iff for a,a9,b,c,b9,c9 st not LIN a,a9,b &
  not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9
  holds b,c // b9,c9
proof
  thus AFP is translational implies for a,a9,b,c,b9,c9 st not LIN a,a9,b & not
LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,
  c // b9,c9
  proof
    assume
A1: AFP is translational;
    let a,a9,b,c,b9,c9;
    assume that
A2: not LIN a,a9,b and
A3: not LIN a,a9,c and
A4: a,a9 // b,b9 and
A5: a,a9 // c,c9 and
A6: a,b // a9,b9 and
A7: a,c // a9,c9;
    set A=Line(a,a9), P=Line(b,b9), C=Line(c,c9);
A8: a in A & a9 in A by AFF_1:15;
A9: c <>c9
    proof
      assume c = c9;
      then c,a // c,a9 by A7,AFF_1:4;
      then LIN c,a,a9 by AFF_1:def 1;
      hence contradiction by A3,AFF_1:6;
    end;
    then
A10: C is being_line by AFF_1:def 3;
A11: b<>b9
    proof
      assume b=b9;
      then b,a // b,a9 by A6,AFF_1:4;
      then LIN b,a,a9 by AFF_1:def 1;
      hence contradiction by A2,AFF_1:6;
    end;
    then
A12: P is being_line by AFF_1:def 3;
A13: a<>a9 by A2,AFF_1:7;
    then
A14: A is being_line by AFF_1:def 3;
A15: c in C by AFF_1:15;
    then
A16: A<>C by A3,A8,A14,AFF_1:21;
A17: A // P by A4,A13,A11,AFF_1:37;
A18: b9 in P & c9 in C by AFF_1:15;
A19: A // C by A5,A13,A9,AFF_1:37;
A20: b in P by AFF_1:15;
    then A<>P by A2,A8,A14,AFF_1:21;
    hence thesis by A1,A6,A7,A8,A20,A15,A18,A14,A12,A10,A17,A19,A16,
AFF_2:def 11;
  end;
  assume
A21: for a,a9,b,c,b9,c9 st not LIN a,a9,b & not LIN a,a9,c & a,a9 // b,
  b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9;
  now
    let A,P,C,a,b,c,a9,b9,c9;
    assume that
A22: A // P and
A23: A // C and
A24: a in A and
A25: a9 in A and
A26: b in P and
A27: b9 in P and
A28: c in C and
A29: c9 in C and
A30: A is being_line and
A31: P is being_line and
A32: C is being_line and
A33: A<>P and
A34: A<>C and
A35: a,b // a9,b9 and
A36: a,c // a9,c9;
A37: a,a9 // b,b9 & a,a9 // c,c9 by A22,A23,A24,A25,A26,A27,A28,A29,AFF_1:39;
A38: now
      assume
A39:  a<>a9;
A40:  not LIN a,a9,c
      proof
        assume LIN a,a9,c;
        then c in A by A24,A25,A30,A39,AFF_1:25;
        hence contradiction by A23,A28,A34,AFF_1:45;
      end;
      not LIN a,a9,b
      proof
        assume LIN a,a9,b;
        then b in A by A24,A25,A30,A39,AFF_1:25;
        hence contradiction by A22,A26,A33,AFF_1:45;
      end;
      hence b,c // b9,c9 by A21,A35,A36,A37,A40;
    end;
    now
      assume
A41:  a=a9;
      then LIN a,c,c9 by A36,AFF_1:def 1;
      then LIN c,c9,a by AFF_1:6;
      then
A42:  c = c9 or a in C by A28,A29,A32,AFF_1:25;
      LIN a,b,b9 by A35,A41,AFF_1:def 1;
      then LIN b,b9,a by AFF_1:6;
      then b=b9 or a in P by A26,A27,A31,AFF_1:25;
      hence b,c // b9,c9 by A22,A23,A24,A33,A34,A42,AFF_1:2,45;
    end;
    hence b,c // b9,c9 by A38;
  end;
  hence thesis by AFF_2:def 11;
end;

theorem Th5:
  ex f st f is translation & f.a=a
proof
  take id the carrier of AFP;
  thus thesis by FUNCT_1:18,TRANSGEO:77;
end;

Lm6: a<>b implies ex y st ( not LIN a,b,x & a,b // x,y & a,x // b,y or (LIN a,
b,x & ex p,q st not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q
,y))
proof
  assume
A1: a<>b;
A2: now
    assume
A3: LIN a,b,x;
    consider p such that
A4: not LIN a,b,p by A1,AFF_1:13;
    consider q such that
A5: a,b // p,q & a,p // b,q by DIRAF:40;
    ex y st p,q // x,y & p,x // q,y by DIRAF:40;
    hence thesis by A3,A4,A5;
  end;
  now
A6: ex y st a,b // x,y & a,x // b,y by DIRAF:40;
    assume not LIN a,b,x;
    hence thesis by A6;
  end;
  hence thesis by A2;
end;

Lm7: a<>b implies ex x st not LIN a,b,x & a,b // x,y & a,x // b,y or LIN a,b,x
& ex p,q st not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y
proof
  assume
A1: a<>b;
A2: now
    assume
A3: LIN a,b,y;
    consider p such that
A4: not LIN a,b,p by A1,AFF_1:13;
    consider q such that
A5: a,b // p,q and
A6: a,p // b,q by DIRAF:40;
A7: now
      assume p=q;
      then p,a // p,b by A6,AFF_1:4;
      then LIN p,a,b by AFF_1:def 1;
      hence contradiction by A4,AFF_1:6;
    end;
    consider x such that
A8: q,p // y,x and
A9: q,y // p,x by DIRAF:40;
A10: p,x // q,y by A9,AFF_1:4;
A11: p,q // x,y by A8,AFF_1:4;
    then a,b // x,y or p=q by A5,AFF_1:5;
    then a,b // y,x by A7,AFF_1:4;
    then LIN a,b,x by A1,A3,AFF_1:9;
    hence thesis by A4,A5,A6,A11,A10;
  end;
  now
    consider x such that
A12: b,a // y,x & b,y // a,x by DIRAF:40;
A13: a,b // x,y & a,x // b,y by A12,AFF_1:4;
    assume not LIN a,b,y;
    then not LIN b,a,y by AFF_1:6;
    then not LIN a,b,x by A12,Lm5;
    hence thesis by A13;
  end;
  hence thesis by A2;
end;

Lm8: AFP is translational & a<>b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p
// b,q & a,p9 // b,q9 & p,q // x,y & p9,q9 // x,y9 & p,x // q,y & p9,x // q9,y9
& not LIN a,b,p & not LIN a,b,p9 & not LIN p,q,p9 implies y=y9
proof
  assume that
A1: AFP is translational and
A2: a<>b and
A3: LIN a,b,x and
A4: a,b // p,q and
A5: a,b // p9,q9 and
A6: a,p // b,q and
A7: a,p9 // b,q9 and
A8: p,q // x,y and
A9: p9,q9 // x,y9 and
A10: p,x // q,y and
A11: p9,x // q9,y9 and
A12: not LIN a,b,p and
A13: not LIN a,b,p9 and
A14: not LIN p,q,p9;
A15: p<>q
  proof
    assume p=q;
    then p,a // p,b by A6,AFF_1:4;
    then LIN p,a,b by AFF_1:def 1;
    hence contradiction by A12,AFF_1:6;
  end;
A16: not LIN p,q,x
  proof
    assume
A17: LIN p,q,x;
    then p,q // p,x by AFF_1:def 1;
    then
A18: p,x // a,b by A4,A15,AFF_1:5;
    a,b // a,x by A3,AFF_1:def 1;
    then p,x // a,x by A2,A18,AFF_1:5;
    then x,p // x,a by AFF_1:4;
    then
A19: LIN x,p,a by AFF_1:def 1;
A20: LIN x,p,x & LIN a,x,b by A3,AFF_1:6,7;
A21: LIN x,p,p by AFF_1:7;
    x<>a by A4,A6,A12,A17,Lm5;
    then LIN x,p,b by A19,A20,AFF_1:11;
    hence contradiction by A3,A12,A19,A21,AFF_1:8;
  end;
A22: p,q // p9,q9 by A2,A4,A5,AFF_1:5;
  then
A23: p9,q9 // x,y by A8,A15,AFF_1:5;
A24: p9<>q9
  proof
    assume p9=q9;
    then p9,a // p9,b by A7,AFF_1:4;
    then LIN p9,a,b by AFF_1:def 1;
    hence contradiction by A13,AFF_1:6;
  end;
A25: not LIN p9,q9,x
  proof
    assume
A26: LIN p9,q9,x;
    then p9,q9 // p9,x by AFF_1:def 1;
    then
A27: p9,x // a,b by A5,A24,AFF_1:5;
    a,b // a,x by A3,AFF_1:def 1;
    then p9,x // a,x by A2,A27,AFF_1:5;
    then x,p9 // x,a by AFF_1:4;
    then
A28: LIN x,p9,a by AFF_1:def 1;
A29: LIN x,p9,x & LIN a,x,b by A3,AFF_1:6,7;
A30: LIN x,p9,p9 by AFF_1:7;
    x<>a by A5,A7,A13,A26,Lm5;
    then LIN x,p9,b by A28,A29,AFF_1:11;
    hence contradiction by A3,A13,A28,A30,AFF_1:8;
  end;
  p,p9 // q,q9 by A1,A4,A5,A6,A7,A12,A13,Th4;
  then p9,x // q9,y by A1,A8,A10,A14,A22,A16,Th4;
  hence thesis by A9,A11,A25,A23,TRANSGEO:76;
end;

theorem Th6:
  (for p,q,r st p<>q & LIN p,q,r holds r = p or r = q) & a,b // p,q
  & a,p // b,q & not LIN a,b,p implies a,q // b,p
proof
  assume that
A1: for p,q,r st p<>q & LIN p,q,r holds r = p or r = q and
A2: a,b // p,q and
A3: a,p // b,q and
A4: not LIN a,b,p;
  consider z such that
A5: q,p // a,z and
A6: q,a // p,z by DIRAF:40;
A7: p<>q
  proof
    assume p=q;
    then p,a // p,b by A3,AFF_1:4;
    then LIN p,a,b by AFF_1:def 1;
    hence contradiction by A4,AFF_1:6;
  end;
A8: not LIN a,p,q
  proof
A9: LIN p,q,p by AFF_1:7;
    assume LIN a,p,q;
    then
A10: LIN p,q,a by AFF_1:6;
    p,q // a,b by A2,AFF_1:4;
    then LIN p,q,b by A7,A10,AFF_1:9;
    hence contradiction by A4,A7,A10,A9,AFF_1:8;
  end;
A11: now
    assume a=z;
    then a,p // a,q by A6,AFF_1:4;
    hence contradiction by A8,AFF_1:def 1;
  end;
  p,q // a,z by A5,AFF_1:4;
  then a,b // a,z by A2,A7,AFF_1:5;
  then
A12: LIN a,b,z by AFF_1:def 1;
  a<>b by A4,AFF_1:7;
  then a=z or b=z by A1,A12;
  hence thesis by A6,A11,AFF_1:4;
end;

Lm9: AFP is translational & a<>b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p
// b,q & a,p9 // b,q9 & p,q // x,y & p9,q9 // x,y9 & p,x // q,y & p9,x // q9,y9
& not LIN a,b,p & not LIN a,b,p9 implies y=y9
proof
  assume that
A1: AFP is translational and
A2: a<>b and
A3: LIN a,b,x and
A4: a,b // p,q and
A5: a,b // p9,q9 and
A6: a,p // b,q and
A7: a,p9 // b,q9 and
A8: p,q // x,y and
A9: p9,q9 // x,y9 and
A10: p,x // q,y and
A11: p9,x // q9,y9 and
A12: not LIN a,b,p and
A13: not LIN a,b,p9;
A14: p<>q
  proof
    assume p=q;
    then p,a // p,b by A6,AFF_1:4;
    then LIN p,a,b by AFF_1:def 1;
    hence contradiction by A12,AFF_1:6;
  end;
  then a,b // x,y by A4,A8,AFF_1:5;
  then
A15: LIN a,b,y by A2,A3,AFF_1:9;
A16: not LIN p,q,x
  proof
    assume LIN p,q,x;
    then p,q // p,x by AFF_1:def 1;
    then a,b // p,x by A4,A14,AFF_1:5;
    then a,b // x,p by AFF_1:4;
    hence contradiction by A2,A3,A12,AFF_1:9;
  end;
A17: now
    assume x=y;
    then x,p // x,q by A10,AFF_1:4;
    then LIN x,p,q by AFF_1:def 1;
    hence contradiction by A16,AFF_1:6;
  end;
A18: p9<>q9
  proof
    assume p9=q9;
    then p9,a // p9,b by A7,AFF_1:4;
    then LIN p9,a,b by AFF_1:def 1;
    hence contradiction by A13,AFF_1:6;
  end;
A19: not LIN q,p,b
  proof
A20: LIN q,p,p by AFF_1:7;
    assume
A21: LIN q,p,b;
    q,p // b,a by A4,AFF_1:4;
    then LIN q,p,a by A14,A21,AFF_1:9;
    hence contradiction by A12,A14,A21,A20,AFF_1:8;
  end;
  now
    assume
A22: LIN p,q,p9;
    p,q // p9,q9 by A2,A4,A5,AFF_1:5;
    then
A23: LIN p,q,q9 by A14,A22,AFF_1:9;
A24: now
      assume
A25:  for x st LIN a,p,x holds x=a or x=p;
      then
A26:  for p,q,r st p<>q & LIN p,q,r holds r = p or r = q by Th1;
A27:  now
        assume
A28:    q=p9;
A29:    now
          a,q // b,p by A4,A6,A12,A26,Th6;
          then
A30:      q,a // p,b by AFF_1:4;
A31:      q,p // a,b by A4,AFF_1:4;
          assume
A32:      a=x;
          then
A33:      q,a // p,y9 & not LIN q,p,a by A11,A14,A18,A16,A23,A25,A28,Th1,
AFF_1:6;
          b=y & q,p // a,y9 by A2,A9,A14,A18,A17,A15,A23,A25,A28,A32,Th1;
          hence thesis by A31,A30,A33,TRANSGEO:76;
        end;
        now
A34:      q,p // b,a & q,b // p,a by A4,A6,AFF_1:4;
          assume
A35:      b=x;
          then
A36:      q,b // p,y9 by A11,A14,A18,A23,A25,A28,Th1;
          a=y & q,p // b,y9 by A2,A9,A14,A18,A17,A15,A23,A25,A28,A35,Th1;
          hence thesis by A19,A34,A36,TRANSGEO:76;
        end;
        hence thesis by A2,A3,A25,A29,Th1;
      end;
      now
        assume
A37:    p=p9;
        then q=q9 by A14,A18,A23,A25,Th1;
        hence thesis by A8,A9,A10,A11,A16,A37,TRANSGEO:76;
      end;
      hence thesis by A14,A22,A25,A27,Th1;
    end;
    now
      given p99 being Element of AFP such that
A38:  LIN a,p,p99 and
A39:  p99<>a and
A40:  p99<>p;
A41:  not LIN p,q,p99
      proof
        assume LIN p,q,p99;
        then
A42:    LIN p,p99,q by AFF_1:6;
        LIN p,p99,p & LIN p,p99,a by A38,AFF_1:6,7;
        then LIN p,q,a by A40,A42,AFF_1:8;
        hence contradiction by A4,A6,A12,Lm5;
      end;
A43:  not LIN p9,q9,p99
      proof
        p,q // p9,q9 by A2,A4,A5,AFF_1:5;
        then
A44:    LIN p,q,q9 by A14,A22,AFF_1:9;
        assume LIN p9,q9,p99;
        hence contradiction by A18,A22,A41,A44,AFF_1:11;
      end;
      consider q99 being Element of AFP such that
A45:  a,b // p99,q99 & a,p99 // b,q99 by DIRAF:40;
      consider y99 being Element of AFP such that
A46:  p99,q99 // x,y99 & p99,x // q99,y99 by DIRAF:40;
A47:  not LIN a,b,p99
      proof
        assume LIN a,b,p99;
        then
A48:    LIN a,p99,b by AFF_1:6;
        LIN a,p99,a & LIN a,p99,p by A38,AFF_1:6,7;
        hence contradiction by A12,A39,A48,AFF_1:8;
      end;
      then y=y99 by A1,A2,A3,A4,A6,A8,A10,A12,A45,A46,A41,Lm8;
      hence thesis by A1,A2,A3,A5,A7,A9,A11,A13,A45,A46,A43,A47,Lm8;
    end;
    hence thesis by A24;
  end;
  hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,Lm8;
end;

Lm10: a<>b & LIN a,b,x & a,b // p,q & a,p // b,q & p,q // x,y & not LIN a,b,p
implies p<>q & LIN a,b,y
proof
  assume that
A1: a<>b & LIN a,b,x and
A2: a,b // p,q and
A3: a,p // b,q and
A4: p,q // x,y and
A5: not LIN a,b,p;
  thus p<>q
  proof
    assume p=q;
    then p,a // p,b by A3,AFF_1:4;
    then LIN p,a,b by AFF_1:def 1;
    hence contradiction by A5,AFF_1:6;
  end;
  then a,b // x,y by A2,A4,AFF_1:5;
  hence thesis by A1,AFF_1:9;
end;

Lm11: AFP is translational & a<>b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,
p // b,q & a,p9 // b,q9 & p,q // x,y & p,x // q,y & p9,q9 // x9,y & p9,x9 // q9
,y & not LIN a,b,p & not LIN a,b,p9 implies x=x9
proof
  assume that
A1: AFP is translational and
A2: a<>b and
A3: LIN a,b,x and
A4: a,b // p,q and
A5: a,b // p9,q9 and
A6: a,p // b,q and
A7: a,p9 // b,q9 and
A8: p,q // x,y and
A9: p,x // q,y and
A10: p9,q9 // x9,y & p9,x9 // q9,y and
A11: not LIN a,b,p and
A12: not LIN a,b,p9;
A13: b,a // q,p & b,a // q9,p9 by A4,A5,AFF_1:4;
A14: b,q // a,p & b,q9 // a,p9 by A6,A7,AFF_1:4;
A15: q9,p9 // y,x9 & q9,y // p9,x9 by A10,AFF_1:4;
  LIN a,b,y by A2,A3,A4,A6,A8,A11,Lm10;
  then
A16: LIN b,a,y by AFF_1:6;
A17: q,p // y,x & q,y // p,x by A8,A9,AFF_1:4;
  ( not LIN b,a,q)& not LIN b,a,q9 by A4,A5,A6,A7,A11,A12,Lm5;
  hence thesis by A1,A2,A16,A13,A14,A17,A15,Lm9;
end;

Lm12: AFP is translational & a<>b implies ex f st f is translation & f.a=b
proof
  defpred X[Element of AFP,Element of AFP] means (not LIN a,b,$1 & a,b // $1,
$2 & a,$1 // b,$2) or (LIN a,b,$1 & (ex p,q st not LIN a,b,p & a,b // p,q & a,p
  // b,q & p,q // $1,$2 & p,$1 // q,$2));
  assume that
A1: AFP is translational and
A2: a<>b;
A3: ex y st X[x,y] by A2,Lm6;
A4: X[x,y] & X[x9,y] implies x=x9
  proof
    assume that
A5: not LIN a,b,x & a,b // x,y & a,x // b,y or (LIN a,b,x & ex p,q st
    not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y) and
A6: not LIN a,b,x9 & a,b // x9,y & a,x9 // b,y or (LIN a,b,x9 & ex p,
    q st not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x9,y & p,x9 // q,y);
A7: now
      assume
A8:   LIN a,b,y;
A9:   not (not LIN a,b,x9 & a,b // x9,y & a,x9 // b,y)
      proof
        assume that
A10:    not LIN a,b,x9 and
A11:    a,b // x9,y and
        a,x9 // b,y;
        a,b // y,x9 by A11,AFF_1:4;
        hence contradiction by A2,A8,A10,AFF_1:9;
      end;
      not (not LIN a,b,x & a,b // x,y & a,x // b,y)
      proof
        assume that
A12:    not LIN a,b,x and
A13:    a,b // x,y and
        a,x // b,y;
        a,b // y,x by A13,AFF_1:4;
        hence contradiction by A2,A8,A12,AFF_1:9;
      end;
      hence thesis by A1,A2,A5,A6,A9,Lm11;
    end;
    now
      assume
A14:  not LIN a,b,y;
      then
A15:  b,y // a,x9 by A2,A6,Lm10,AFF_1:4;
A16:  b,y // a,x & b,a // y,x9 by A2,A5,A6,A14,Lm10,AFF_1:4;
      ( not LIN b,a,y)& b,a // y,x by A2,A5,A14,Lm5,Lm10,AFF_1:4;
      hence thesis by A16,A15,TRANSGEO:76;
    end;
    hence thesis by A7;
  end;
A17: ex x st X[x,y] by A2,Lm7;
A18: X[x,y] & X[x,y9] implies y=y9 by A1,A2,Lm9,TRANSGEO:76;
  ex f st for x,y holds f.x=y iff X[x,y] from TRANSGEO:sch 1(A3,A17, A4,A18
  );
  then consider f such that
A19: for x,y holds f.x=y iff not LIN a,b,x & a,b // x,y & a,x // b,y or
LIN a,b,x & ex p,q st not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,
  x // q,y;
A20: a,b // x,f.x
  proof
    set y=f.x;
    now
      assume
A21:  LIN a,b,x;
      then consider p,q such that
A22:  not LIN a,b,p and
A23:  a,b // p,q and
A24:  a,p // b,q and
A25:  p,q // x,y and
      p,x // q,y by A19;
      p<>q by A2,A21,A22,A23,A24,A25,Lm10;
      hence thesis by A23,A25,AFF_1:5;
    end;
    hence thesis by A19;
  end;
  for x,y holds x,y // f.x,f.y
  proof
    let x,y;
A26: now
A27:  ex x9 st y,f.y // x,x9 & y,x // f.y,x9 by DIRAF:40;
      assume that
A28:  LIN a,b,x and
A29:  not LIN a,b,y;
      a,b // y,f.y & a,y // b,f.y by A19,A29;
      then y,x // f.y,f.x by A19,A28,A29,A27;
      hence thesis by AFF_1:4;
    end;
A30: now
A31:  ex y9 st x,f.x // y,y9 & x,y // f.x,y9 by DIRAF:40;
      assume that
A32:  not LIN a,b,x and
A33:  LIN a,b,y;
      a,b // x,f.x & a,x // b,f.x by A19,A32;
      hence thesis by A19,A32,A33,A31;
    end;
A34: now
      assume
A35:  LIN a,b,x & LIN a,b,y;
      then LIN a,b,f.x & LIN a,b,f.y by A2,A20,AFF_1:9;
      then
A36:  a,b // f.x,f.y by AFF_1:10;
      a,b // x,y by A35,AFF_1:10;
      hence thesis by A2,A36,AFF_1:5;
    end;
    now
      assume
A37:  ( not LIN a,b,x)& not LIN a,b,y;
      then
A38:  a,b // x,f.x & a,b // y,f.y by A19;
      a,x // b,f.x & a,y // b,f.y by A19,A37;
      hence thesis by A1,A37,A38,Th4;
    end;
    hence thesis by A34,A26,A30;
  end;
  then
A39: f is dilatation by TRANSGEO:64;
A40: f.a=b
  proof
A41: LIN a,b,a by AFF_1:7;
    consider p such that
A42: not LIN a,b,p by A2,AFF_1:13;
    consider q such that
A43: a,b // p,q & a,p // b,q by DIRAF:40;
    p,a // q,b & p,q // a,b by A43,AFF_1:4;
    hence thesis by A19,A42,A43,A41;
  end;
  x,f.x // y,f.y
  proof
    a,b // x,f.x & a,b // y,f.y by A20;
    hence thesis by A2,AFF_1:5;
  end;
  then f is translation by A39,TRANSGEO:78;
  hence thesis by A40;
end;

theorem Th7:
  AFP is translational implies ex f st f is translation & f.a=b
proof
  assume
A1: AFP is translational;
  a=b implies thesis by Th5;
  hence thesis by A1,Lm12;
end;

theorem
  (for a,b ex f st f is translation & f.a=b) implies AFP is translational
proof
  assume
A1: for a,b ex f st f is translation & f.a=b;
  now
    let a,a9,b,c,b9,c9;
    consider f such that
A2: f is translation and
A3: f.a=a9 by A1;
A4: f is dilatation by A2,TRANSGEO:def 11;
    assume ( not LIN a,a9,b)& not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 &
    a,b // a9,b9 & a,c // a9,c9;
    then b9=f.b & c9=f.c by A2,A3,Th3;
    hence b,c // b9,c9 by A4,TRANSGEO:64;
  end;
  hence thesis by Th4;
end;

theorem Th9:
  f is translation & g is translation & not LIN a,f.a,g.a implies f*g=g*f
proof
  assume that
A1: f is translation and
A2: g is translation;
A3: g is dilatation by A2,TRANSGEO:def 11;
  then
A4: a,f.a // g.a,g.(f.a) by TRANSGEO:64;
  assume
A5: not LIN a,f.a,g.a;
  a,g.a // f.a,g.(f.a) by A2,A3,TRANSGEO:78;
  then f.(g.a)=g.(f.a) by A1,A5,A4,Th3;
  then (f*g).a=g.(f.a) by FUNCT_2:15;
  then
A6: (f*g).a=(g*f).a by FUNCT_2:15;
  f*g is translation & g*f is translation by A1,A2,TRANSGEO:82;
  hence thesis by A6,TRANSGEO:80;
end;

theorem Th10:
  AFP is translational & f is translation & g is translation implies f*g=g*f
proof
  assume that
A1: AFP is translational and
A2: f is translation and
A3: g is translation;
A4: g is dilatation by A3,TRANSGEO:def 11;
  now
    set a = the Element of AFP;
    assume that
A5: f<>id the carrier of AFP and
A6: g<>id the carrier of AFP;
A7: a<>f.a by A2,A5,TRANSGEO:def 11;
A8: a<>g.a by A3,A6,TRANSGEO:def 11;
    now
      consider b such that
A9:   not LIN a,f.a,b by A7,AFF_1:13;
      consider h such that
A10:  h is translation and
A11:  h.a=b by A1,Th7;
A12:  h *g is translation by A3,A10,TRANSGEO:82;
      assume
A13:  LIN a,f.a,g.a;
      not LIN a,f.a,h.(g.a)
      proof
A14:    not LIN a,g.a,b
        proof
          assume
A15:      LIN a,g.a,b;
          LIN a,g.a,f.a & LIN a,g.a,a by A13,AFF_1:6,7;
          hence contradiction by A8,A9,A15,AFF_1:8;
        end;
        then (g*h).a=(h*g).a by A3,A10,A11,Th9;
        then (g*h).a=h.(g.a) by FUNCT_2:15;
        then
A16:    g.b=h.(g.a) by A11,FUNCT_2:15;
        assume
A17:    LIN a,f.a,h.(g.a);
        a,g.a // b,g.b & a,b // g.a,g.b by A3,A4,TRANSGEO:64,78;
        then LIN a,f.a,a & not LIN g.a,a,h.(g.a) by A14,A16,Lm5,AFF_1:7;
        hence contradiction by A7,A13,A17,AFF_1:8;
      end;
      then
A18:  not LIN a,f.a,(h*g).a by FUNCT_2:15;
      h*(f*g)=(h*f)*g by RELAT_1:36
        .=(f*h)*g by A2,A9,A10,A11,Th9
        .=f*(h*g) by RELAT_1:36
        .=(h*g)*f by A2,A12,A18,Th9
        .=h*(g*f) by RELAT_1:36;
      hence thesis by TRANSGEO:5;
    end;
    hence thesis by A2,A3,Th9;
  end;
  hence thesis by TRANSGEO:4;
end;

theorem Th11:
  f is translation & g is translation & p,f.p // p,g.p implies p,f
  .p // p,(f*g).p
proof
  assume that
A1: f is translation and
A2: g is translation and
A3: p,f.p // p,g.p;
A4: f is dilatation by A1,TRANSGEO:def 11;
A5: now
    assume g<>id the carrier of AFP;
    then
A6: g.p<>p by A2,TRANSGEO:def 11;
    p,g.p // f.p,f.(g.p) by A4,TRANSGEO:64;
    then p,f.p // f.p,f.(g.p) by A3,A6,AFF_1:5;
    then f.p,p // f.p,f.(g.p) by AFF_1:4;
    then LIN f.p,p,f.(g.p) by AFF_1:def 1;
    then LIN p,f.p,f.(g.p) by AFF_1:6;
    then p,f.p // p,f.(g.p) by AFF_1:def 1;
    hence thesis by FUNCT_2:15;
  end;
  now
    assume g=id the carrier of AFP;
    then f*g=f by FUNCT_2:17;
    hence thesis by AFF_1:2;
  end;
  hence thesis by A5;
end;

theorem
  AFP is Fanoian & AFP is translational & f is translation implies ex g
  st g is translation & g*g=f
proof
  assume that
A1: AFP is Fanoian and
A2: AFP is translational and
A3: f is translation;
A4: now
    set a = the Element of AFP;
    set b=f.a;
    assume f<>id the carrier of AFP;
    then a<>b by A3,TRANSGEO:def 11;
    then consider c such that
A5: not LIN a,b,c by AFF_1:13;
    consider d such that
A6: c,b // a,d and
A7: c,a // b,d by DIRAF:40;
    not LIN c,b,a by A5,AFF_1:6;
    then consider p such that
A8: LIN b,a,p and
A9: LIN c,d,p by A1,A6,A7,Th2;
    consider f1 being Permutation of the carrier of AFP such that
A10: f1 is translation and
A11: f1.p=a by A2,Th7;
    consider f2 being Permutation of the carrier of AFP such that
A12: f2 is translation and
A13: f2.p=b by A2,Th7;
A14: f1*f2 is translation by A10,A12,TRANSGEO:82;
A15: LIN p,c,d by A9,AFF_1:6;
    then
A16: p,c // p,d by AFF_1:def 1;
A17: now
      assume p,c // p,a;
      then LIN p,c,a by AFF_1:def 1;
      then
A18:  LIN p,a,c by AFF_1:6;
      LIN p,a,a & LIN p,a,b by A8,AFF_1:6,7;
      then p=a by A5,A18,AFF_1:8;
      then a,c // c,b or a=d by A6,A16,AFF_1:5;
      then c,a // c,b or a=d by AFF_1:4;
      then LIN c,a,b or a=d by AFF_1:def 1;
      then a,c // a,b by A5,A7,AFF_1:4,6;
      then LIN a,c,b by AFF_1:def 1;
      hence contradiction by A5,AFF_1:6;
    end;
    consider f3 being Permutation of the carrier of AFP such that
A19: f3 is translation and
A20: f3.p=c by A2,Th7;
    (f3)" is translation by A19,TRANSGEO:81;
    then
A21: f1*(f3)" is translation by A10,TRANSGEO:82;
    LIN p,a,b by A8,AFF_1:6;
    then p,f1.p // p,f2.p by A11,A13,AFF_1:def 1;
    then
A22: p,a // p,(f1*f2).p by A10,A11,A12,Th11;
    consider f4 being Permutation of the carrier of AFP such that
A23: f4 is translation and
A24: f4.p=d by A2,Th7;
    f4.((f2)".b)=f4.p by A13,TRANSGEO:2;
    then
A25: (f4*f2").b=d by A24,FUNCT_2:15;
    consider h such that
A26: h is translation and
A27: h.c = a by A2,Th7;
    not LIN c,a,b by A5,AFF_1:6;
    then
A28: h.b=d by A6,A7,A26,A27,Th3;
    f1.((f3)".c)=f1.p by A20,TRANSGEO:2;
    then (f1*(f3)").c = a by A11,FUNCT_2:15;
    then
A29: f1*(f3)"=h by A26,A27,A21,TRANSGEO:80;
A30: (f2)" is translation by A12,TRANSGEO:81;
    then f4*f2" is translation by A23,TRANSGEO:82;
    then f1*f3"=f4*f2" by A26,A28,A29,A25,TRANSGEO:80;
    then f1*(f3"*f3)=(f4*f2")*f3 by RELAT_1:36;
    then f1*(id the carrier of AFP)=(f4*f2")*f3 by FUNCT_2:61;
    then f1=(f4*f2")*f3 by FUNCT_2:17
      .=f4*(f2"*f3) by RELAT_1:36
      .=f4*(f3*f2") by A2,A19,A30,Th10
      .=(f4*f3)*f2" by RELAT_1:36;
    then
A31: f1*f2=(f4*f3)*(f2"*f2) by RELAT_1:36
      .=(f4*f3)*(id the carrier of AFP) by FUNCT_2:61
      .=f4*f3 by FUNCT_2:17;
    p,f3.p // p,f4.p by A20,A24,A15,AFF_1:def 1;
    then p,c // p,(f3*f4).p by A19,A20,A23,Th11;
    then p,c // p,(f1*f2).p by A2,A19,A23,A31,Th10;
    then p=(f1*f2).p by A22,A17,AFF_1:5;
    then f1"*(f1*f2)=f1"*(id the carrier of AFP) by A14,TRANSGEO:def 11;
    then (f1"*f1)*f2=f1"*(id the carrier of AFP) by RELAT_1:36;
    then (id the carrier of AFP)*f2=f1"*(id the carrier of AFP) by FUNCT_2:61;
    then f2=f1"*(id the carrier of AFP) by FUNCT_2:17;
    then
A32: (f2*f2).a=(f2*f1").a by FUNCT_2:17
      .=f2.(f1".a) by FUNCT_2:15
      .=b by A11,A13,TRANSGEO:2;
    f2*f2 is translation by A12,TRANSGEO:82;
    hence thesis by A3,A12,A32,TRANSGEO:80;
  end;
  now
    set g=id the carrier of AFP;
A33: g is translation & g*g=id the carrier of AFP by FUNCT_2:17,TRANSGEO:77;
    assume f=id the carrier of AFP;
    hence thesis by A33;
  end;
  hence thesis by A4;
end;

theorem Th13:
  AFP is Fanoian & f is translation & f*f=id the carrier of AFP
  implies f=id the carrier of AFP
proof
  set a = the Element of AFP;
  assume that
A1: AFP is Fanoian and
A2: f is translation and
A3: f*f=id the carrier of AFP;
  assume f<>id the carrier of AFP;
  then a<>f.a by A2,TRANSGEO:def 11;
  then consider b such that
A4: not LIN a,f.a,b by AFF_1:13;
A5: f is dilatation by A2,TRANSGEO:def 11;
  then
A6: a,b // f.a,f.b by TRANSGEO:64;
  f.b,a // f.(f.b),f.a by A5,TRANSGEO:64;
  then f.b,a // (f*f).b,f.a by FUNCT_2:15;
  then f.b,a // b,f.a by A3,FUNCT_1:18;
  then
A7: a,f.b // f.a,b by AFF_1:4;
  a,f.a // b,f.b by A2,A5,TRANSGEO:78;
  hence contradiction by A1,A4,A6,A7,Def1;
end;

theorem
  AFP is translational & AFP is Fanoian & f1 is translation & f2 is
  translation & g=f1*f1 & g=f2*f2 implies f1=f2
proof
  assume that
A1: AFP is translational and
A2: AFP is Fanoian and
A3: f1 is translation and
A4: f2 is translation and
A5: g=f1*f1 & g=f2*f2;
  set h=f2"*f1;
A6: f2" is translation by A4,TRANSGEO:81;
  h*h=f2"*(f1*(f2"*f1)) by RELAT_1:36
    .=f2"*((f1*f2")*f1) by RELAT_1:36
    .=f2"*((f2"*f1)*f1) by A1,A3,A6,Th10
    .=f2"*(f2"*(f1*f1)) by RELAT_1:36
    .=(f2"*f2")*(f1*f1) by RELAT_1:36
    .=g"*g by A5,FUNCT_1:44
    .=id the carrier of AFP by FUNCT_2:61;
  then f2"*f1=id the carrier of AFP by A2,A3,A6,Th13,TRANSGEO:82;
  then f2"*f1=f2"*f2 by FUNCT_2:61;
  hence thesis by TRANSGEO:5;
end;