let AFS be AffinSpace; :: thesis: for f being Permutation of the carrier of AFS st f is dilatation holds

f " is dilatation

let f be Permutation of the carrier of AFS; :: 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 AFS; :: 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 AFS holds x,y // (f ") . x,(f ") . y

hence
f " is dilatation
by Th68; :: thesis: verumlet x, y be Element of AFS; :: 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, Th68;

hence x,y // (f ") . x,(f ") . y by AFF_1:4; :: 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, Th68;

hence x,y // (f ") . x,(f ") . y by AFF_1:4; :: thesis: verum