let AFS be AffinSpace; :: thesis: for f being Permutation of the carrier of AFS st f is dilatation holds
for a, b, c being Element of AFS holds
( LIN a,b,c iff LIN f . a,f . b,f . c )
let f be Permutation of the carrier of AFS; :: thesis: ( f is dilatation implies for a, b, c being Element of AFS 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 AFS holds
( LIN a,b,c iff LIN f . a,f . b,f . c )
let a, b, c be Element of AFS; :: 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, Th72;
hence ( LIN a,b,c iff LIN f . a,f . b,f . c ) by AFF_1:def 1; :: thesis: verum