let m, n be Nat; :: thesis: for K being Field
for P being finite without_zero Subset of NAT
for M being Matrix of m,n,K st P c= Seg m & lines M is linearly-independent holds
lines (Segm M,P,(Seg n)) is linearly-independent
let K be Field; :: thesis: for P being finite without_zero Subset of NAT
for M being Matrix of m,n,K st P c= Seg m & lines M is linearly-independent holds
lines (Segm M,P,(Seg n)) is linearly-independent
let P be finite without_zero Subset of NAT ; :: thesis: for M being Matrix of m,n,K st P c= Seg m & lines M is linearly-independent holds
lines (Segm M,P,(Seg n)) is linearly-independent
let M be Matrix of m,n,K; :: thesis: ( P c= Seg m & lines M is linearly-independent implies lines (Segm M,P,(Seg n)) is linearly-independent )
assume that
A1: P c= Seg m and
A2: lines M is linearly-independent ; :: thesis: lines (Segm M,P,(Seg n)) is linearly-independent
( card (Seg n) = n & lines (Segm M,P,(Seg n)) c= lines M ) by A1, Th118, FINSEQ_1:78;
hence lines (Segm M,P,(Seg n)) is linearly-independent by A2, VECTSP_7:2; :: thesis: verum