theorem Th50:
for
l,
m,
n being
Nat for
K being
Field for
A being
Matrix of
n,
m,
K for
B being
Matrix of
n,
l,
K for
N being
finite without_zero Subset of
NAT st
card N = n &
N c= Seg m &
n > 0 &
Segm (
A,
(Seg n),
N)
= 1. (
K,
n) holds
ex
X being
Matrix of
m,
l,
K st
(
Segm (
X,
((Seg m) \ N),
(Seg l))
= 0. (
K,
(m -' n),
l) &
Segm (
X,
N,
(Seg l))
= B &
X in Solutions_of (
A,
B) )