let AFP be AffinPlane; :: thesis: for f being Permutation of the carrier of AFP st AFP is Fanoian & AFP is translational & f is translation holds
ex g being Permutation of the carrier of AFP st
( g is translation & g * g = f )
let f be Permutation of the carrier of AFP; :: thesis: ( AFP is Fanoian & AFP is translational & f is translation implies ex g being Permutation of the carrier of AFP st
( g is translation & g * g = f ) )
assume that
A1: AFP is Fanoian and
A2: AFP is translational and
A3: f is translation ; :: thesis: ex g being Permutation of the carrier of AFP st
( g is translation & g * g = f )

A4: now

consider a being Element of AFP;
set b = f . a;
assume f <> id the carrier of AFP ; :: thesis: ex g being Permutation of the carrier of AFP st
( g is translation & g * g = f )
then a <> f . a by A3, TRANSGEO:def 11;
then consider c being Element of AFP such that
A5: not LIN a,f . a,c by AFF_1:22;
consider d being Element of AFP such that
A6: c,f . a // a,d and
A7: c,a // f . a,d by DIRAF:47;
not LIN c,f . a,a by A5, AFF_1:15;
then consider p being Element of AFP such that
A8: LIN f . a,a,p and
A9: LIN c,d,p by A1, A6, A7, Th4;
consider f1 being Permutation of the carrier of AFP such that
A10: f1 is translation and
A11: f1 . p = a by A2, Th9;
consider f2 being Permutation of the carrier of AFP such that
A12: f2 is translation and
A13: f2 . p = f . a by A2, Th9;
A14: f1 * f2 is translation by A10, A12, TRANSGEO:105;
A15: LIN p,c,d by A9, AFF_1:15;
then A16: p,c // p,d by AFF_1:def 1;

A17: now

assume p,c // p,a ; :: thesis: contradiction
then LIN p,c,a by AFF_1:def 1;
then A18: LIN p,a,c by AFF_1:15;
( LIN p,a,a & LIN p,a,f . a ) by A8, AFF_1:15, AFF_1:16;
then p = a by A5, A18, AFF_1:17;
then ( a,c // c,f . a or a = d ) by A6, A16, AFF_1:14;
then ( c,a // c,f . a or a = d ) by AFF_1:13;
then ( LIN c,a,f . a or a = d ) by AFF_1:def 1;
then a,c // a,f . a by A5, A7, AFF_1:13, AFF_1:15;
then LIN a,c,f . a by AFF_1:def 1;
hence contradiction by A5, AFF_1:15; :: thesis: verum

end;

consider f3 being Permutation of the carrier of AFP such that
A19: f3 is translation and
A20: f3 . p = c by A2, Th9;
f3 " is translation by A19, TRANSGEO:104;
then A21: f1 * (f3 " ) is translation by A10, TRANSGEO:105;
LIN p,a,f . a by A8, AFF_1:15;
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, Th13;
consider f4 being Permutation of the carrier of AFP such that
A23: f4 is translation and
A24: f4 . p = d by A2, Th9;
f4 . ((f2 " ) . (f . a)) = f4 . p by A13, TRANSGEO:4;
then A25: (f4 * (f2 " )) . (f . a) = d by A24, FUNCT_2:21;
consider h being Permutation of the carrier of AFP such that
A26: h is translation and
A27: h . c = a by A2, Th9;
not LIN c,a,f . a by A5, AFF_1:15;
then A28: h . (f . a) = d by A6, A7, A26, A27, Th5;
f1 . ((f3 " ) . c) = f1 . p by A20, TRANSGEO:4;
then (f1 * (f3 " )) . c = a by A11, FUNCT_2:21;
then A29: f1 * (f3 " ) = h by A26, A27, A21, TRANSGEO:103;
A30: f2 " is translation by A12, TRANSGEO:104;
then f4 * (f2 " ) is translation by A23, TRANSGEO:105;
then f1 * (f3 " ) = f4 * (f2 " ) by A26, A28, A29, A25, TRANSGEO:103;
then f1 * ((f3 " ) * f3) = (f4 * (f2 " )) * f3 by RELAT_1:55;
then f1 * (id the carrier of AFP) = (f4 * (f2 " )) * f3 by FUNCT_2:88;
then f1 = (f4 * (f2 " )) * f3 by FUNCT_2:23
.= f4 * ((f2 " ) * f3) by RELAT_1:55
.= f4 * (f3 * (f2 " )) by A2, A19, A30, Th12
.= (f4 * f3) * (f2 " ) by RELAT_1:55 ;
then A31: f1 * f2 = (f4 * f3) * ((f2 " ) * f2) by RELAT_1:55
.= (f4 * f3) * (id the carrier of AFP) by FUNCT_2:88
.= f4 * f3 by FUNCT_2:23 ;
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, Th13;
then p,c // p,(f1 * f2) . p by A2, A19, A23, A31, Th12;
then p = (f1 * f2) . p by A22, A17, AFF_1:14;
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:55;
then (id the carrier of AFP) * f2 = (f1 " ) * (id the carrier of AFP) by FUNCT_2:88;
then f2 = (f1 " ) * (id the carrier of AFP) by FUNCT_2:23;
then A32: (f2 * f2) . a = (f2 * (f1 " )) . a by FUNCT_2:23
.= f2 . ((f1 " ) . a) by FUNCT_2:21
.= f . a by A11, A13, TRANSGEO:4 ;
f2 * f2 is translation by A12, TRANSGEO:105;
hence ex g being Permutation of the carrier of AFP st
( g is translation & g * g = f ) by A3, A12, A32, TRANSGEO:103; :: thesis: verum

end;

now

set g = id the carrier of AFP;
A33: ( id the carrier of AFP is translation & (id the carrier of AFP) * (id the carrier of AFP) = id the carrier of AFP ) by FUNCT_2:23, TRANSGEO:99;
assume f = id the carrier of AFP ; :: thesis: ex g being Permutation of the carrier of AFP st
( g is translation & g * g = f )
hence ex g being Permutation of the carrier of AFP st
( g is translation & g * g = f ) by A33; :: thesis: verum

end;

hence ex g being Permutation of the carrier of AFP st
( g is translation & g * g = f ) by A4; :: thesis: verum