let V be RealLinearSpace; for A, B, C being Element of V st A <> C & A,B,C are_collinear holds
A - B = (affine-ratio (A,B,C)) * (A - C)
let A, B, C be Element of V; ( A <> C & A,B,C are_collinear implies A - B = (affine-ratio (A,B,C)) * (A - C) )
assume that
A1:
A <> C
and
A2:
A,B,C are_collinear
; A - B = (affine-ratio (A,B,C)) * (A - C)
A - B =
- (B - A)
by RLVECT_1:33
.=
- ((affine-ratio (A,B,C)) * (C - A))
by Def02, A1, A2
.=
(- 1) * ((affine-ratio (A,B,C)) * (C - A))
by RLVECT_1:16
.=
((- 1) * (affine-ratio (A,B,C))) * (C - A)
by RLVECT_1:def 7
.=
(affine-ratio (A,B,C)) * ((- 1) * (C - A))
by RLVECT_1:def 7
.=
(affine-ratio (A,B,C)) * (- (C - A))
by RLVECT_1:16
.=
(affine-ratio (A,B,C)) * (A - C)
by RLVECT_1:33
;
hence
A - B = (affine-ratio (A,B,C)) * (A - C)
; verum