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

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:113;
hence [:(Seg (card P)),(Seg (card Q)):] = Indices (Segm A,P,Q) by A2, MATRIX_1:23; :: 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_1:24; :: 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:45;
then A3: (Sgm Q) " Y c= Seg (card Q) by RELAT_1:167;
ex n being Nat st P c= Seg n by Th43;
then dom (Sgm P) = Seg (card P) by FINSEQ_3:45;
then (Sgm P) " X c= Seg (card P) by RELAT_1:167;
hence [:((Sgm P) " X),((Sgm Q) " Y):] c= Indices (Segm A,P,Q) by A3, A1, ZFMISC_1:119; :: thesis: verum