let AFS be AffinSpace; :: thesis: for f being Permutation of the carrier of AFS holds
( f is dilatation iff for a, b being Element of AFS holds a,b // f . a,f . b )
let f be Permutation of the carrier of AFS; :: thesis: ( f is dilatation iff for a, b being Element of AFS holds a,b // f . a,f . b )
thus ( f is dilatation implies for a, b being Element of AFS holds a,b // f . a,f . b ) :: thesis: ( ( for a, b being Element of AFS holds a,b // f . a,f . b ) implies f is dilatation )

proof

assume f is dilatation ; :: thesis: for a, b being Element of AFS holds a,b // f . a,f . b
then A1: f is_DIL_of AFS by Def10;
let a, b be Element of AFS; :: thesis: a,b // f . a,f . b
thus a,b // f . a,f . b by A1, Th35; :: thesis: verum

end;

assume for a, b being Element of AFS holds a,b // f . a,f . b ; :: thesis: f is dilatation
then f is_DIL_of AFS by Th35;
hence f is dilatation by Def10; :: thesis: verum