let AFP be AffinPlane; :: thesis: for g, f1, f2 being Permutation of the carrier of AFP st AFP is translational & AFP is Fanoian & 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 & f1 is translation & f2 is translation & g = f1 * f1 & g = f2 * f2 implies f1 = f2 )
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 ) ; :: thesis: f1 = f2
set h = (f2 ") * f1;
A6: f2 " is translation by A4, TRANSGEO:85;
((f2 ") * f1) * ((f2 ") * f1) = (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:86;
then (f2 ") * f1 = (f2 ") * f2 by FUNCT_2:61;
hence f1 = f2 by TRANSGEO:5; :: thesis: verum