let AFS be AffinSpace; :: thesis: for f being Permutation of the carrier of AFS st f is dilatation holds
( f is translation iff for x, y being Element of AFS holds x,f . x // y,f . y )
let f be Permutation of the carrier of AFS; :: thesis: ( f is dilatation implies ( f is translation iff for x, y being Element of AFS holds x,f . x // y,f . y ) )
assume A1: f is dilatation ; :: thesis: ( f is translation iff for x, y being Element of AFS holds x,f . x // y,f . y )
then ( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y ) by Th93;
hence ( f is translation iff for x, y being Element of AFS holds x,f . x // y,f . y ) by A1, Def11; :: thesis: verum