let AFP be AffinPlane; :: thesis: for a being Element of AFP

for f, g being Permutation of the carrier of AFP st f is translation & g is translation & not LIN a,f . a,g . a holds

f * g = g * f

let a be Element of AFP; :: thesis: for f, g being Permutation of the carrier of AFP st f is translation & g is translation & not LIN a,f . a,g . a holds

f * g = g * f

let f, g be Permutation of the carrier of AFP; :: thesis: ( f is translation & g is translation & not LIN a,f . a,g . a implies f * g = g * f )

assume that

A1: f is translation and

A2: g is translation ; :: thesis: ( LIN a,f . a,g . a or f * g = g * f )

A3: g is dilatation by A2, TRANSGEO:def 11;

then A4: a,f . a // g . a,g . (f . a) by TRANSGEO:68;

assume A5: not LIN a,f . a,g . a ; :: thesis: f * g = g * f

a,g . a // f . a,g . (f . a) by A2, A3, TRANSGEO:82;

then f . (g . a) = g . (f . a) by A1, A5, A4, Th3;

then (f * g) . a = g . (f . a) by FUNCT_2:15;

then A6: (f * g) . a = (g * f) . a by FUNCT_2:15;

( f * g is translation & g * f is translation ) by A1, A2, TRANSGEO:86;

hence f * g = g * f by A6, TRANSGEO:84; :: thesis: verum

for f, g being Permutation of the carrier of AFP st f is translation & g is translation & not LIN a,f . a,g . a holds

f * g = g * f

let a be Element of AFP; :: thesis: for f, g being Permutation of the carrier of AFP st f is translation & g is translation & not LIN a,f . a,g . a holds

f * g = g * f

let f, g be Permutation of the carrier of AFP; :: thesis: ( f is translation & g is translation & not LIN a,f . a,g . a implies f * g = g * f )

assume that

A1: f is translation and

A2: g is translation ; :: thesis: ( LIN a,f . a,g . a or f * g = g * f )

A3: g is dilatation by A2, TRANSGEO:def 11;

then A4: a,f . a // g . a,g . (f . a) by TRANSGEO:68;

assume A5: not LIN a,f . a,g . a ; :: thesis: f * g = g * f

a,g . a // f . a,g . (f . a) by A2, A3, TRANSGEO:82;

then f . (g . a) = g . (f . a) by A1, A5, A4, Th3;

then (f * g) . a = g . (f . a) by FUNCT_2:15;

then A6: (f * g) . a = (g * f) . a by FUNCT_2:15;

( f * g is translation & g * f is translation ) by A1, A2, TRANSGEO:86;

hence f * g = g * f by A6, TRANSGEO:84; :: thesis: verum