let OAS be OAffinSpace; :: thesis: for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation holds
f * g is dilatation
let f, g be Permutation of the carrier of OAS; :: 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

let x, y be Element of OAS; :: 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:21;

A3: now

assume g . x = g . y ; :: thesis: x,y '||' (f * g) . x,(f * g) . y
then x = y by FUNCT_2:85;
hence x,y '||' (f * g) . x,(f * g) . y by DIRAF:25; :: thesis: verum

end;

( x,y '||' g . x,g . y & g . x,g . y '||' f . (g . x),f . (g . y) ) by A1, Th51;
hence x,y '||' (f * g) . x,(f * g) . y by A2, A3, DIRAF:28; :: thesis: verum

end;

hence f * g is dilatation by Th51; :: thesis: verum