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

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