let OAS be OAffinSpace; :: thesis: for f, g being Permutation of the carrier of OAS st f is translation & g is translation holds
f * g is translation
let f, g be Permutation of the carrier of OAS; :: 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 Th44;
now :: thesis: ( f * g <> id the carrier of OAS implies f * g is translation )
assume A4: f * g <> id the carrier of OAS ; :: thesis: f * g is translation
for x being Element of OAS holds (f * g) . x <> x
proof
given x being Element of OAS 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, Th56;
then f * g = f * (f ") by A2, A6, Th55;
hence contradiction by A4, FUNCT_2:61; :: thesis: verum
end;
hence f * g is translation by A3; :: thesis: verum
end;
hence f * g is translation by A3; :: thesis: verum