let OAS be OAffinSpace; :: thesis: for f, g being Permutation of the carrier of OAS st f is positive_dilatation & g is negative_dilatation holds
( f * g is negative_dilatation & g * f is negative_dilatation )
let f, g be Permutation of the carrier of OAS; :: thesis: ( f is positive_dilatation & g is negative_dilatation implies ( f * g is negative_dilatation & g * f is negative_dilatation ) )
assume that
A1: f is positive_dilatation and
A2: g is negative_dilatation ; :: thesis: ( f * g is negative_dilatation & g * f is negative_dilatation )
thus for x, y being Element of OAS holds x,y // (f * g) . y,(f * g) . x :: according to TRANSGEO:def 7 :: thesis: g * f is negative_dilatation

proof

let x, y be Element of OAS; :: thesis: x,y // (f * g) . y,(f * g) . x
set x' = g . x;
set y' = g . y;
A3: ( (f * g) . x = f . (g . x) & (f * g) . y = f . (g . y) ) by FUNCT_2:21;
A4: x,y // g . y,g . x by A2, Def7;
A5: g . y,g . x // f . (g . y),f . (g . x) by A1, Th42;

now

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

end;

hence x,y // (f * g) . y,(f * g) . x by A3, A4, A5, DIRAF:6; :: thesis: verum

end;

thus for x, y being Element of OAS holds x,y // (g * f) . y,(g * f) . x :: according to TRANSGEO:def 7 :: thesis: verum

proof

let x, y be Element of OAS; :: thesis: x,y // (g * f) . y,(g * f) . x
set x' = f . x;
set y' = f . y;
A6: ( (g * f) . x = g . (f . x) & (g * f) . y = g . (f . y) ) by FUNCT_2:21;
A7: x,y // f . x,f . y by A1, Th42;
A8: f . x,f . y // g . (f . y),g . (f . x) by A2, Def7;

now

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

end;

hence x,y // (g * f) . y,(g * f) . x by A6, A7, A8, DIRAF:6; :: thesis: verum

end;