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