let AFS be AffinSpace; :: thesis: for f being Permutation of the carrier of AFS st f is translation holds
f " is translation
let f be Permutation of the carrier of AFS; :: thesis: ( f is translation implies f " is translation )
assume A1: f is translation ; :: thesis: f " is translation
then f is dilatation by Def11;
then A2: f " is dilatation by Th87;
A3: ( f = id the carrier of AFS implies f " = id the carrier of AFS ) by FUNCT_1:67;

now

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

end;

hence f " is translation by A1, A2, A3, Def11; :: thesis: verum