let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS st f is translation holds
f " is translation
let f be Permutation of the carrier of OAS; :: thesis: ( f is translation implies f " is translation )

A1: now

assume A2: for x being Element of OAS holds f . x <> x ; :: thesis: for y being Element of OAS holds not (f " ) . y = y
given y being Element of OAS such that A3: (f " ) . y = y ; :: thesis: contradiction
f . y = y by A3, Th4;
hence contradiction by A2; :: thesis: verum

end;

assume A4: f is translation ; :: thesis: f " is translation
then f is dilatation by Def9;
then A5: f " is dilatation by Th56;
( f = id the carrier of OAS implies f " = id the carrier of OAS ) by FUNCT_1:67;
hence f " is translation by A4, A5, A1, Def9; :: thesis: verum