let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS holds
( f is dilatation iff for a, b being Element of OAS holds a,b '||' f . a,f . b )
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation iff for a, b being Element of OAS holds a,b '||' f . a,f . b )

A1: now

assume f is dilatation ; :: thesis: for a, b being Element of OAS holds a,b '||' f . a,f . b
then A2: f is_FormalIz_of lambda the CONGR of OAS by Def8;
let a, b be Element of OAS; :: thesis: a,b '||' f . a,f . b
[[a,b],[(f . a),(f . b)]] in lambda the CONGR of OAS by A2, Def2;
hence a,b '||' f . a,f . b by DIRAF:23; :: thesis: verum

end;

now

assume A3: for a, b being Element of OAS holds a,b '||' f . a,f . b ; :: thesis: f is dilatation

now

let a, b be Element of OAS; :: thesis: [[a,b],[(f . a),(f . b)]] in lambda the CONGR of OAS
a,b '||' f . a,f . b by A3;
hence [[a,b],[(f . a),(f . b)]] in lambda the CONGR of OAS by DIRAF:23; :: thesis: verum

end;

then f is_FormalIz_of lambda the CONGR of OAS by Def2;
hence f is dilatation by Def8; :: thesis: verum

end;

hence ( f is dilatation iff for a, b being Element of OAS holds a,b '||' f . a,f . b ) by A1; :: thesis: verum