let K be Field; :: thesis:
let A be Matrix of K; :: thesis:
let N be finite without_zero Subset of NAT; :: thesis:
assume that
A1: N c= dom A and
A2: for i being Nat st i in (dom A) \ N holds
Line (A,i) = (width A) |-> (0. K) ; :: thesis:
set w = width A;
set l = len A;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;
set S = Segm (A9,N,(Seg (width A9)));
consider U being finite Subset of ((width A) -VectSp_over K) such that
A3: U is linearly-independent and
A4: U c= lines A9 and
A5: card U = the_rank_of A9 by MATRIX13:123;
A6: U c= lines (Segm (A9,N,(Seg (width A9))))

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: x in U ; :: thesis:
consider Ni being Nat such that
A8: Ni in Seg (len A) and
A9: x = Line (A9,Ni) by A4, A7, MATRIX13:103;
A10: dom A = Seg (len A) by FINSEQ_1:def 3;
A11: Ni in N

end;

rng (Sgm N) = N by FINSEQ_1:def 14;
then consider i being object such that
A12: i in dom (Sgm N) and
A13: (Sgm N) . i = Ni by A11, FUNCT_1:def 3;
reconsider i = i as Element of NAT by A12;
A14: dom (Sgm N) = Seg (card N) by FINSEQ_3:40;
then Line ((Segm (A9,N,(Seg (width A9)))),i) = x by A9, A12, A13, MATRIX13:48;
hence x in lines (Segm (A9,N,(Seg (width A9)))) by A12, A14, MATRIX13:103; :: thesis:

end;

end;