let AFP be AffinPlane; 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; ( 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 )
; 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; verum