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 )

then f is dilatation ;

then A5: f " is dilatation by Th70;

( f = id the carrier of AFS implies f " = id the carrier of AFS ) by FUNCT_1:45;

hence f " is translation by A4, A5, A1; :: thesis: verum

f " is translation

let f be Permutation of the carrier of AFS; :: thesis: ( f is translation implies f " is translation )

A1: now :: thesis: ( ( for x being Element of AFS holds f . x <> x ) implies for y being Element of AFS holds not (f ") . y = y )

assume A4:
f is translation
; :: thesis: f " is translation assume A2:
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 A3: (f ") . y = y ; :: thesis: contradiction

f . y = y by A3, Th2;

hence contradiction by A2; :: thesis: verum

end;given y being Element of AFS such that A3: (f ") . y = y ; :: thesis: contradiction

f . y = y by A3, Th2;

hence contradiction by A2; :: thesis: verum

then f is dilatation ;

then A5: f " is dilatation by Th70;

( f = id the carrier of AFS implies f " = id the carrier of AFS ) by FUNCT_1:45;

hence f " is translation by A4, A5, A1; :: thesis: verum