theorem Th38:
for
i,
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) holds
X in Solutions_of (
(RLine (A9,i,(a * (Line (A9,i))))),
(RLine (B9,i,(a * (Line (B9,i))))))