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 object ; :: 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;
then m <> 0 ;
then width M = n by Th1;
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:40;
then (Sgm P) . i in rng (Sgm P) by A3, FUNCT_1:def 3;
hence x in lines M by A1, A4, A2, A5, Th103; :: thesis: verum