theorem Th36: :: EUCLIDLP:36

for a1, a2, b1, b2 being Real
for n being Nat
for y2, x1, x2, y1, y1 being Element of REAL n st y1,y2 are_lindependent2 & y1 = (a1 * x1) + (a2 * x2) & y2 = (b1 * x1) + (b2 * x2) holds
ex c1, c2, d1, d2 being Real st
( x1 = (c1 * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) )