theorem Th40: :: MATRIX15:40

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