theorem Th35: :: EUCLIDLP:35

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