let AFP be AffinPlane; for f being Permutation of the carrier of AFP st AFP is Fanoian & f is translation & f * f = id the carrier of AFP holds
f = id the carrier of AFP
let f be Permutation of the carrier of AFP; ( AFP is Fanoian & f is translation & f * f = id the carrier of AFP implies f = id the carrier of AFP )
set a = the Element of AFP;
assume that
A1:
AFP is Fanoian
and
A2:
f is translation
and
A3:
f * f = id the carrier of AFP
; f = id the carrier of AFP
assume
f <> id the carrier of AFP
; contradiction
then
the Element of AFP <> f . the Element of AFP
by A2, TRANSGEO:def 11;
then consider b being Element of AFP such that
A4:
not LIN the Element of AFP,f . the Element of AFP,b
by AFF_1:13;
A5:
f is dilatation
by A2, TRANSGEO:def 11;
then A6:
the Element of AFP,b // f . the Element of AFP,f . b
by TRANSGEO:68;
f . b, the Element of AFP // f . (f . b),f . the Element of AFP
by A5, TRANSGEO:68;
then
f . b, the Element of AFP // (f * f) . b,f . the Element of AFP
by FUNCT_2:15;
then
f . b, the Element of AFP // b,f . the Element of AFP
by A3;
then A7:
the Element of AFP,f . b // f . the Element of AFP,b
by AFF_1:4;
the Element of AFP,f . the Element of AFP // b,f . b
by A2, A5, TRANSGEO:82;
hence
contradiction
by A1, A4, A6, A7; verum