theorem :: EUCLIDLP:89

for a1, a2, a3, b1, b2, b3 being Real
for n being Nat
for x, x1, x2, x3 being Element of REAL n st x2 - x1,x3 - x1 are_lindependent2 & (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (b1 + b2) + b3 = 1 & x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) holds
( a1 = b1 & a2 = b2 & a3 = b3 )