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 that
A1: f is dilatation and
A2: 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 x' = g . x;
set y' = g . y;
A3: (f * g) . x = f . (g . x) by FUNCT_2:21;
A4: (f * g) . y = f . (g . y) by FUNCT_2:21;
A5: ( x,y '||' g . x,g . y & g . x,g . y '||' f . (g . x),f . (g . y) ) by A1, A2, Th51;

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;

hence x,y '||' (f * g) . x,(f * g) . y by A3, A4, A5, DIRAF:28; :: thesis: verum

end;

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