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 )
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
consider a being Element of AFP;
assume f <> id the carrier of AFP ; :: thesis: contradiction
then a <> f . a by A2, TRANSGEO:def 11;
then consider b being Element of AFP such that
A4: not LIN a,f . a,b by AFF_1:22;
A5: f is dilatation by A2, TRANSGEO:def 11;
then f . b,a // f . (f . b),f . a by TRANSGEO:85;
then f . b,a // (f * f) . b,f . a by FUNCT_2:21;
then f . b,a // b,f . a by A3, FUNCT_1:35;
then ( a,b // f . a,f . b & a,f . a // b,f . b & a,f . b // f . a,b ) by A2, A5, AFF_1:13, TRANSGEO:85, TRANSGEO:100;
hence contradiction by A1, A4, Def1; :: thesis: verum