let D be non empty set ; :: thesis: for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st card P = card Q holds
( [:P,Q:] c= Indices A iff ( P c= Seg (len A) & Q c= Seg (width A) ) )
let A be Matrix of D; :: thesis: for P, Q being finite without_zero Subset of NAT st card P = card Q holds
( [:P,Q:] c= Indices A iff ( P c= Seg (len A) & Q c= Seg (width A) ) )
let P, Q be finite without_zero Subset of NAT; :: thesis: ( card P = card Q implies ( [:P,Q:] c= Indices A iff ( P c= Seg (len A) & Q c= Seg (width A) ) ) )
A1: Indices A = [:(Seg (len A)),(Seg (width A)):] by FINSEQ_1:def 3;
assume A2: card P = card Q ; :: thesis: ( [:P,Q:] c= Indices A iff ( P c= Seg (len A) & Q c= Seg (width A) ) )
thus ( [:P,Q:] c= Indices A implies ( P c= Seg (len A) & Q c= Seg (width A) ) ) :: thesis: ( P c= Seg (len A) & Q c= Seg (width A) implies [:P,Q:] c= Indices A )

proof

assume A3: [:P,Q:] c= Indices A ; :: thesis: ( P c= Seg (len A) & Q c= Seg (width A) )

per cases ( [:P,Q:] <> {} or [:P,Q:] = {} ) ;

suppose [:P,Q:] <> {} ; :: thesis: ( P c= Seg (len A) & Q c= Seg (width A) )

hence ( P c= Seg (len A) & Q c= Seg (width A) ) by A1, A3, ZFMISC_1:114; :: thesis: verum

end;

suppose A4: [:P,Q:] = {} ; :: thesis: ( P c= Seg (len A) & Q c= Seg (width A) )

then A5: Q = {} by A2, CARD_1:27, ZFMISC_1:90;
P = {} by A2, A4, CARD_1:27, ZFMISC_1:90;
hence ( P c= Seg (len A) & Q c= Seg (width A) ) by A5; :: thesis: verum

end;

end;

end;

thus ( P c= Seg (len A) & Q c= Seg (width A) implies [:P,Q:] c= Indices A ) by A1, ZFMISC_1:96; :: thesis: verum