let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation holds
f " is dilatation
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation implies f " is dilatation )
assume A1: f is dilatation ; :: thesis: f " is dilatation

now :: thesis: for x, y being Element of OAS holds x,y '||' (f ") . x,(f ") . y

let x, y be Element of OAS; :: thesis: x,y '||' (f ") . x,(f ") . y
set x9 = (f ") . x;
set y9 = (f ") . y;
( f . ((f ") . x) = x & f . ((f ") . y) = y ) by Th2;
then (f ") . x,(f ") . y '||' x,y by A1, Th34;
hence x,y '||' (f ") . x,(f ") . y by DIRAF:22; :: thesis: verum

end;

hence f " is dilatation by Th34; :: thesis: verum