let AFS be AffinSpace; :: thesis: for f, g being Permutation of the carrier of AFS st f is dilatation & g is dilatation holds
f * g is dilatation
let f, g be Permutation of the carrier of AFS; :: thesis: ( f is dilatation & g is dilatation implies f * g is dilatation )
assume A1: ( f is dilatation & g is dilatation ) ; :: thesis: f * g is dilatation
now :: thesis: for x, y being Element of AFS holds x,y // (f * g) . x,(f * g) . y
let x, y be Element of AFS; :: thesis: x,y // (f * g) . x,(f * g) . y
set x9 = g . x;
set y9 = g . y;
A2: ( (f * g) . x = f . (g . x) & (f * g) . y = f . (g . y) ) by FUNCT_2:15;
A3: now :: thesis: ( g . x = g . y implies x,y // (f * g) . x,(f * g) . y )
assume g . x = g . y ; :: thesis: x,y // (f * g) . x,(f * g) . y
then x = y by FUNCT_2:58;
hence x,y // (f * g) . x,(f * g) . y by AFF_1:3; :: thesis: verum
end;
( x,y // g . x,g . y & g . x,g . y // f . (g . x),f . (g . y) ) by A1, Th68;
hence x,y // (f * g) . x,(f * g) . y by A2, A3, AFF_1:5; :: thesis: verum
end;
hence f * g is dilatation by Th68; :: thesis: verum