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

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

hence
f " is dilatation
by Th34; :: thesis: verumlet 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;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