let AFP be AffinPlane; :: thesis: 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; :: thesis: ( 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 ; :: thesis: f = id the carrier of AFP
assume f <> id the carrier of AFP ; :: thesis: 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; :: thesis: verum