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 )
set S = Segm M,P,(Seg n);
assume A1: P c= Seg m ; :: thesis: lines (Segm M,P,(Seg n)) c= lines M
then A2: rng (Sgm P) = P by FINSEQ_1:def 13;
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
A3: i in Seg (card P) and
A4: x = Line (Segm M,P,(Seg n)),i by Th103;
Seg m <> {} by A1, A3, FINSEQ_1:4;
then m <> 0 ;
then width M = n by Th1, FINSEQ_1:4;
then A5: Line (Segm M,P,(Seg n)),i = Line M,((Sgm P) . i) by A3, Th48;
dom (Sgm P) = Seg (card P) by A1, FINSEQ_3:45;
then (Sgm P) . i in rng (Sgm P) by A3, FUNCT_1:def 5;
hence x in lines M by A1, A4, A2, A5, Th103; :: thesis: verum