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 holds
lines (Segm M,P,(Seg n)) c= lines M
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 holds
lines (Segm M,P,(Seg n)) c= lines M
let P be finite without_zero Subset of NAT ; :: thesis: for M being Matrix of m,n,K st P c= Seg m holds
lines (Segm M,P,(Seg n)) c= lines M
let M be Matrix of m,n,K; :: thesis: ( P c= Seg m implies lines (Segm M,P,(Seg n)) c= lines M )
assume A1: P c= Seg m ; :: thesis: lines (Segm M,P,(Seg n)) c= lines M
set S = Segm M,P,(Seg n);
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in lines (Segm M,P,(Seg n)) or x in lines M )
assume x in lines (Segm M,P,(Seg n)) ; :: thesis: x in lines M
then consider i being Nat such that
A2: ( i in Seg (card P) & x = Line (Segm M,P,(Seg n)),i ) by Th103;
dom (Sgm P) = Seg (card P) by A1, FINSEQ_3:45;
then A3: ( (Sgm P) . i in rng (Sgm P) & rng (Sgm P) = P ) by A1, A2, FINSEQ_1:def 13, FUNCT_1:def 5;
Seg m <> {} by A1, A2, FINSEQ_1:4;
then width M = n by Th1, FINSEQ_1:4;
then Line (Segm M,P,(Seg n)),i = Line M,((Sgm P) . i) by A2, Th48;
hence x in lines M by A1, A2, A3, Th103; :: thesis: verum