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 by FINSEQ_1:57;
hence lines (Segm (M,P,(Seg n))) is linearly-independent by A1, A2, Th118, VECTSP_7:1; :: thesis: verum