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

let x, y be Element of OAS; :: thesis: x,y '||' (f " ) . x,(f " ) . y
set x' = (f " ) . x;
set y' = (f " ) . y;
( f . ((f " ) . x) = x & f . ((f " ) . y) = y ) by Th4;
then (f " ) . x,(f " ) . y '||' x,y by A1, Th51;
hence x,y '||' (f " ) . x,(f " ) . y by DIRAF:27; :: thesis: verum

end;

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