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
A3: f is dilatation by A1, Def9;
g is dilatation by A2, Def9;
then A4: f * g is dilatation by A3, Th57;

now

assume A5: 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 A6: (f * g) . x = x ; :: thesis: contradiction
f . (g . x) = x by A6, FUNCT_2:21;
then ( g . x = (f " ) . x & f " is translation ) by A1, Th4, Th71;
then f * g = f * (f " ) by A2, Th70;
hence contradiction by A5, FUNCT_2:88; :: thesis: verum

end;

hence f * g is translation by A4, Def9; :: thesis: verum

end;

hence f * g is translation by A4, Def9; :: thesis: verum