let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation holds
for a, b, c being Element of OAS holds
( a,b,c are_collinear iff f . a,f . b,f . c are_collinear )
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation implies for a, b, c being Element of OAS holds
( a,b,c are_collinear iff f . a,f . b,f . c are_collinear ) )
assume A1: f is dilatation ; :: thesis: for a, b, c being Element of OAS holds
( a,b,c are_collinear iff f . a,f . b,f . c are_collinear )
let a, b, c be Element of OAS; :: thesis: ( a,b,c are_collinear iff f . a,f . b,f . c are_collinear )
( a,b '||' a,c iff f . a,f . b '||' f . a,f . c ) by A1, Th45;
hence ( a,b,c are_collinear iff f . a,f . b,f . c are_collinear ) by DIRAF:def 5; :: thesis: verum