let K be Field; :: thesis: for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds
( card P <= len M & card Q <= width M )
let M be Matrix of K; :: thesis: for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds
( card P <= len M & card Q <= width M )
let P, Q be finite without_zero Subset of NAT ; :: thesis: ( [:P,Q:] c= Indices M & card P = card Q implies ( card P <= len M & card Q <= width M ) )
assume A1: ( [:P,Q:] c= Indices M & card P = card Q ) ; :: thesis: ( card P <= len M & card Q <= width M )
( P c= Seg (len M) & Q c= Seg (width M) ) by A1, Th67;
then ( card P <= card (Seg (len M)) & card Q <= card (Seg (width M)) & card (Seg (len M)) = len M ) by FINSEQ_1:78, NAT_1:44;
hence ( card P <= len M & card Q <= width M ) by FINSEQ_1:78; :: thesis: verum