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
( LIN a,b,c iff LIN f . a,f . b,f . c )
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation implies for a, b, c being Element of OAS holds
( LIN a,b,c iff LIN f . a,f . b,f . c ) )
assume A1: f is dilatation ; :: thesis: for a, b, c being Element of OAS holds
( LIN a,b,c iff LIN f . a,f . b,f . c )
let a, b, c be Element of OAS; :: thesis: ( LIN a,b,c iff LIN f . a,f . b,f . c )
( a,b '||' a,c iff f . a,f . b '||' f . a,f . c ) by A1, Th58;
hence ( LIN a,b,c iff LIN f . a,f . b,f . c ) by DIRAF:def 5; :: thesis: verum