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;
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