let AFS be AffinSpace; :: thesis: for f, g being Permutation of the carrier of AFS st f is translation & g is translation holds

f * g is translation

let f, g be Permutation of the carrier of AFS; :: thesis: ( f is translation & g is translation implies f * g is translation )

assume that

A1: f is translation and

A2: g is translation ; :: thesis: f * g is translation

( f is dilatation & g is dilatation ) by A1, A2;

then A3: f * g is dilatation by Th71;

f * g is translation

let f, g be Permutation of the carrier of AFS; :: thesis: ( f is translation & g is translation implies f * g is translation )

assume that

A1: f is translation and

A2: g is translation ; :: thesis: f * g is translation

( f is dilatation & g is dilatation ) by A1, A2;

then A3: f * g is dilatation by Th71;

now :: thesis: ( f * g <> id the carrier of AFS implies f * g is translation )

hence
f * g is translation
by A3; :: thesis: verumassume A4:
f * g <> id the carrier of AFS
; :: thesis: f * g is translation

for x being Element of AFS holds (f * g) . x <> x

end;for x being Element of AFS holds (f * g) . x <> x

proof

hence
f * g is translation
by A3; :: thesis: verum
given x being Element of AFS such that A5:
(f * g) . x = x
; :: thesis: contradiction

f . (g . x) = x by A5, FUNCT_2:15;

then A6: g . x = (f ") . x by Th2;

f " is translation by A1, Th85;

then f * g = f * (f ") by A2, A6, Th84;

hence contradiction by A4, FUNCT_2:61; :: thesis: verum

end;f . (g . x) = x by A5, FUNCT_2:15;

then A6: g . x = (f ") . x by Th2;

f " is translation by A1, Th85;

then f * g = f * (f ") by A2, A6, Th84;

hence contradiction by A4, FUNCT_2:61; :: thesis: verum