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

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