theorem Th67:
for
m,
n being
Nat for
K being
Field for
A being
Matrix of
n,
m,
K for
N being
finite without_zero Subset of
NAT st
card N = n &
N c= Seg m &
Segm (
A,
(Seg n),
N)
= 1. (
K,
n) &
n > 0 &
m -' n > 0 holds
ex
MVectors being
Matrix of
m -' n,
m,
K st
(
Segm (
MVectors,
(Seg (m -' n)),
((Seg m) \ N))
= 1. (
K,
(m -' n)) &
Segm (
MVectors,
(Seg (m -' n)),
N)
= - ((Segm (A,(Seg n),((Seg m) \ N))) @) &
Lin (lines MVectors) = Space_of_Solutions_of A )