theorem Th65: :: MATRIX15:65

for m, n being Nat
for K being Field
for a being Element of K
for A9 being Matrix of m,n,K
for i, j being Nat st j in Seg m & n > 0 & ( i = j implies a <> - (1_ K) ) holds
Space_of_Solutions_of A9 = Space_of_Solutions_of (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))))