let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation holds
( f is translation iff for x, y being Element of OAS holds x,f . x '||' y,f . y )
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation implies ( f is translation iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) )
assume A1: f is dilatation ; :: thesis: ( f is translation iff for x, y being Element of OAS holds x,f . x '||' y,f . y )
then ( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) by Th62;
hence ( f is translation iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) by A1, Def9; :: thesis: verum