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) ) ) )
assume A1: card P = card Q ; :: thesis: ( [:P,Q:] c= Indices A iff ( P c= Seg (len A) & Q c= Seg (width A) ) )
A2: Indices A = [:(Seg (len A)),(Seg (width A)):] by FINSEQ_1:def 3;
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 A2, A3, ZFMISC_1:138; :: thesis: verum

end;

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

then ( card P = 0 or card Q = 0 ) by CARD_1:47, ZFMISC_1:113;
then ( P = {} & Q = {} ) by A1;
hence ( P c= Seg (len A) & Q c= Seg (width A) ) by XBOOLE_1:2; :: thesis: verum

end;

end;

end;

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