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 :: thesis: ( ( for x being Element of OAS holds f . x <> x ) implies for y being Element of OAS holds not (f ") . y = y )

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, Th2;
hence contradiction by A2; :: thesis: verum

end;

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