theorem Th39:
for
i,
j,
k,
m,
n being
Nat for
K being
Field for
a being
Element of
K for
X being
Matrix of
K for
A9 being
Matrix of
m,
n,
K for
B9 being
Matrix of
m,
k,
K st
X in Solutions_of (
A9,
B9) &
j in Seg m holds
X in Solutions_of (
(RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),
(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))