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

now

let x, y be Element of OAS; :: thesis: x,y '||' f . x,f . y
( x,y // f . x,f . y or x,y // f . y,f . x ) by A1, Def7, Th42;
hence x,y '||' f . x,f . y by DIRAF:def 4; :: thesis: verum

end;

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