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);
consider n being Nat such that
A1: P c= Seg n by Th43;
consider m being Nat such that
A2: Q c= Seg m by Th43;
( dom (Sgm P) = Seg (card P) & dom (Sgm Q) = Seg (card Q) ) by A1, A2, FINSEQ_3:45;
then A3: ( (Sgm P) " X c= Seg (card P) & (Sgm Q) " Y c= Seg (card Q) ) by RELAT_1:167;

now

per cases ( card P = 0 or card P > 0 ) ;

suppose A4: card P = 0 ; :: thesis: [:(Seg (card P)),(Seg (card Q)):] = Indices (Segm A,P,Q)

then [:(Seg (card P)),(Seg (card Q)):] = {} by FINSEQ_1:4, ZFMISC_1:113;
hence [:(Seg (card P)),(Seg (card Q)):] = Indices (Segm A,P,Q) by A4, 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;

hence [:((Sgm P) " X),((Sgm Q) " Y):] c= Indices (Segm A,P,Q) by A3, ZFMISC_1:119; :: thesis: verum