let AFS be AffinSpace; :: thesis: for x, y being Element of AFS
for f being Permutation of the carrier of AFS st f is dilatation & LIN x,f . x,y holds
LIN x,f . x,f . y
let x, y be Element of AFS; :: thesis: for f being Permutation of the carrier of AFS st f is dilatation & LIN x,f . x,y holds
LIN x,f . x,f . y
let f be Permutation of the carrier of AFS; :: thesis: ( f is dilatation & LIN x,f . x,y implies LIN x,f . x,f . y )
assume A1: f is dilatation ; :: thesis: ( not LIN x,f . x,y or LIN x,f . x,f . y )
assume A2: LIN x,f . x,y ; :: thesis: LIN x,f . x,f . y

now :: thesis: ( x <> y implies LIN x,f . x,f . y )

assume A3: x <> y ; :: thesis: LIN x,f . x,f . y
( x,f . x // x,y & x,y // f . x,f . y ) by A1, A2, Th68, AFF_1:def 1;
then x,f . x // f . x,f . y by A3, AFF_1:5;
then f . x,x // f . x,f . y by AFF_1:4;
then LIN f . x,x,f . y by AFF_1:def 1;
hence LIN x,f . x,f . y by AFF_1:6; :: thesis: verum

end;

hence LIN x,f . x,f . y by AFF_1:7; :: thesis: verum