let AFS be AffinSpace; 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; ( f is dilatation & g is dilatation implies f * g is dilatation )
assume A1:
( f is dilatation & g is dilatation )
; f * g is dilatation
now for x, y being Element of AFS holds x,y // (f * g) . x,(f * g) . ylet x,
y be
Element of
AFS;
x,y // (f * g) . x,(f * g) . yset 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 ( g . x = g . y implies x,y // (f * g) . x,(f * g) . y )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;
verum end;
hence
f * g is dilatation
by Th68; verum