let AFP be AffinPlane; :: thesis: for g, f1, f2 being Permutation of the carrier of AFP st AFP is translational & AFP is Fanoian & g is translation & f1 is translation & f2 is translation & g = f1 * f1 & g = f2 * f2 holds
f1 = f2
let g, f1, f2 be Permutation of the carrier of AFP; :: thesis: ( AFP is translational & AFP is Fanoian & g is translation & f1 is translation & f2 is translation & g = f1 * f1 & g = f2 * f2 implies f1 = f2 )
assume that
A1: ( AFP is translational & AFP is Fanoian ) and
g is translation and
A2: f1 is translation and
A3: f2 is translation and
A4: g = f1 * f1 and
A5: g = f2 * f2 ; :: thesis: f1 = f2
set h = (f2 " ) * f1;
A6: f2 " is translation by A3, TRANSGEO:104;
((f2 " ) * f1) * ((f2 " ) * f1) = (f2 " ) * (f1 * ((f2 " ) * f1)) by RELAT_1:55
.= (f2 " ) * ((f1 * (f2 " )) * f1) by RELAT_1:55
.= (f2 " ) * (((f2 " ) * f1) * f1) by A1, A2, A6, Th12
.= (f2 " ) * ((f2 " ) * (f1 * f1)) by RELAT_1:55
.= ((f2 " ) * (f2 " )) * (f1 * f1) by RELAT_1:55
.= (g " ) * g by A4, A5, FUNCT_1:66
.= id the carrier of AFP by FUNCT_2:88 ;
then (f2 " ) * f1 = id the carrier of AFP by A1, A2, A6, Th15, TRANSGEO:105;
then (f2 " ) * f1 = (f2 " ) * f2 by FUNCT_2:88;
hence f1 = f2 by TRANSGEO:13; :: thesis: verum