consider L being line of V such that
A3:
A in L
and
A4:
B in L
and
A5:
C in L
by A2;
consider P, Q being Element of V such that
A6:
L = Line (P,Q)
by RLTOPSP1:def 15;
A7:
Line (P,Q) = { (((1 - r) * P) + (r * Q)) where r is Real : verum }
by RLTOPSP1:def 14;
consider a being Real such that
A8:
A = ((1 - a) * P) + (a * Q)
by A3, A6, A7;
consider b being Real such that
A9:
B = ((1 - b) * P) + (b * Q)
by A4, A6, A7;
consider c being Real such that
A10:
C = ((1 - c) * P) + (c * Q)
by A5, A6, A7;
A11:
a - c <> 0
by A8, A10, A1;
set k = (a - b) / (a - c);
B - A =
(a - b) * (P - Q)
by A8, A9, Lm01
.=
(((a - b) / (a - c)) * (a - c)) * (P - Q)
by A11, XCMPLX_1:87
.=
((a - b) / (a - c)) * ((a - c) * (P - Q))
by RLVECT_1:def 7
.=
((a - b) / (a - c)) * (C - A)
by A8, A10, Lm01
;
hence
ex b1 being Real st B - A = b1 * (C - A)
; verum