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 & AFP is translational ) and
A2: f is translation ; :: thesis: ex g being Permutation of the carrier of AFP st
( g is translation & g * g = f )

A3: now

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

end;

now

assume A6: f <> id the carrier of AFP ; :: thesis: ex g being Permutation of the carrier of AFP st
( g is translation & g * g = f )
consider a being Element of AFP;
set b = f . a;
a <> f . a by A2, A6, TRANSGEO:def 11;
then consider c being Element of AFP such that
A7: not LIN a,f . a,c by AFF_1:22;
A8: ( not LIN c,a,f . a & not LIN c,f . a,a ) by A7, AFF_1:15;
consider d being Element of AFP such that
A9: ( c,f . a // a,d & c,a // f . a,d ) by DIRAF:47;
consider p being Element of AFP such that
A10: LIN f . a,a,p and
A11: LIN c,d,p by A1, A8, A9, Th4;
consider h being Permutation of the carrier of AFP such that
A12: h is translation and
A13: h . c = a by A1, Th9;
A14: h . (f . a) = d by A8, A9, A12, A13, Th5;
consider f1 being Permutation of the carrier of AFP such that
A15: f1 is translation and
A16: f1 . p = a by A1, Th9;
consider f2 being Permutation of the carrier of AFP such that
A17: f2 is translation and
A18: f2 . p = f . a by A1, Th9;
consider f3 being Permutation of the carrier of AFP such that
A19: f3 is translation and
A20: f3 . p = c by A1, Th9;
consider f4 being Permutation of the carrier of AFP such that
A21: f4 is translation and
A22: f4 . p = d by A1, Th9;
A23: f2 " is translation by A17, TRANSGEO:104;
A24: f1 * f2 = f4 * f3

proof

f1 . ((f3 " ) . c) = f1 . p by A20, TRANSGEO:4;
then A25: (f1 * (f3 " )) . c = a by A16, FUNCT_2:21;
f3 " is translation by A19, TRANSGEO:104;
then f1 * (f3 " ) is translation by A15, TRANSGEO:105;
then A26: f1 * (f3 " ) = h by A12, A13, A25, TRANSGEO:103;
f4 . ((f2 " ) . (f . a)) = f4 . p by A18, TRANSGEO:4;
then A27: (f4 * (f2 " )) . (f . a) = d by A22, FUNCT_2:21;
f4 * (f2 " ) is translation by A21, A23, TRANSGEO:105;
then f1 * (f3 " ) = f4 * (f2 " ) by A12, A14, A26, A27, 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 A1, A19, A23, Th12
.= (f4 * f3) * (f2 " ) by RELAT_1:55 ;
then 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 ;
hence f1 * f2 = f4 * f3 ; :: thesis: verum

end;

A28: LIN p,c,d by A11, AFF_1:15;
then A29: p,c // p,d by AFF_1:def 1;
p,f3 . p // p,f4 . p by A20, A22, A28, AFF_1:def 1;
then p,c // p,(f3 * f4) . p by A19, A20, A21, Th13;
then A30: p,c // p,(f1 * f2) . p by A1, A19, A21, A24, Th12;
LIN p,a,f . a by A10, AFF_1:15;
then p,f1 . p // p,f2 . p by A16, A18, AFF_1:def 1;
then A31: p,a // p,(f1 * f2) . p by A15, A16, A17, Th13;

now

assume p,c // p,a ; :: thesis: contradiction
then LIN p,c,a by AFF_1:def 1;
then ( LIN p,a,c & LIN p,a,a & LIN p,a,f . a ) by A10, AFF_1:15, AFF_1:16;
then p = a by A7, AFF_1:17;
then ( a,c // c,f . a or a = d ) by A9, A29, 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 A7, A9, AFF_1:13, AFF_1:15;
then LIN a,c,f . a by AFF_1:def 1;
hence contradiction by A7, AFF_1:15; :: thesis: verum

end;

then ( p = (f1 * f2) . p & f1 * f2 is translation ) by A15, A17, A30, A31, AFF_1:14, TRANSGEO:105;
then (f1 " ) * (f1 * f2) = (f1 " ) * (id the carrier of AFP) by 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 (f2 * f2) . a = (f2 * (f1 " )) . a by FUNCT_2:23
.= f2 . ((f1 " ) . a) by FUNCT_2:21
.= f . a by A16, A18, TRANSGEO:4 ;
then ( (f2 * f2) . a = f . a & f2 * f2 is translation ) by A17, TRANSGEO:105;
hence ex g being Permutation of the carrier of AFP st
( g is translation & g * g = f ) by A2, A17, TRANSGEO:103; :: thesis: verum

end;

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