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 :: thesis: for x, y being Element of OAS holds x,y '||' (f * g) . x,(f * g) . y
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: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 DIRAF:20; :: thesis: verum
end;
( x,y '||' g . x,g . y & g . x,g . y '||' f . (g . x),f . (g . y) ) by A1, Th34;
hence x,y '||' (f * g) . x,(f * g) . y by A2, A3, DIRAF:23; :: thesis: verum
end;
hence f * g is dilatation by Th34; :: thesis: verum