let X, Y be set ; :: thesis: for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT holds [:((Sgm P) " X),((Sgm Q) " Y):] c= Indices (Segm (A,P,Q))
let D be non empty set ; :: thesis: for A being Matrix of D
for P, Q being finite without_zero Subset of NAT holds [:((Sgm P) " X),((Sgm Q) " Y):] c= Indices (Segm (A,P,Q))
let A be Matrix of D; :: thesis: for P, Q being finite without_zero Subset of NAT holds [:((Sgm P) " X),((Sgm Q) " Y):] c= Indices (Segm (A,P,Q))
let P, Q be finite without_zero Subset of NAT; :: thesis: [:((Sgm P) " X),((Sgm Q) " Y):] c= Indices (Segm (A,P,Q))
set SP = Sgm P;
set SQ = Sgm Q;
set I = Indices (Segm (A,P,Q));
A1: now :: thesis: [:(Seg (card P)),(Seg (card Q)):] = Indices (Segm (A,P,Q))
per cases ( card P = 0 or card P > 0 ) ;
suppose A2: card P = 0 ; :: thesis: [:(Seg (card P)),(Seg (card Q)):] = Indices (Segm (A,P,Q))
then Seg (card P) = {} ;
then [:(Seg (card P)),(Seg (card Q)):] = {} by ZFMISC_1:90;
hence [:(Seg (card P)),(Seg (card Q)):] = Indices (Segm (A,P,Q)) by A2, MATRIX_0:22; :: thesis: verum
end;
suppose card P > 0 ; :: thesis: [:(Seg (card P)),(Seg (card Q)):] = Indices (Segm (A,P,Q))
hence [:(Seg (card P)),(Seg (card Q)):] = Indices (Segm (A,P,Q)) by MATRIX_0:23; :: thesis: verum
end;
end;
end;
ex m being Nat st Q c= Seg m by Th43;
then dom (Sgm Q) = Seg (card Q) by FINSEQ_3:40;
then A3: (Sgm Q) " Y c= Seg (card Q) by RELAT_1:132;
ex n being Nat st P c= Seg n by Th43;
then dom (Sgm P) = Seg (card P) by FINSEQ_3:40;
then (Sgm P) " X c= Seg (card P) by RELAT_1:132;
hence [:((Sgm P) " X),((Sgm Q) " Y):] c= Indices (Segm (A,P,Q)) by A3, A1, ZFMISC_1:96; :: thesis: verum