let OAS be OAffinSpace; 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; ( 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
; 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; ( 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; verum