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

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