let K be Field; 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; 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; ( [:P,Q:] c= Indices M & card P = card Q implies ( card P <= len M & card Q <= width M ) )
assume that
A1:
[:P,Q:] c= Indices M
and
A2:
card P = card Q
; ( card P <= len M & card Q <= width M )
Q c= Seg (width M)
by A1, A2, Th67;
then A3:
card Q <= card (Seg (width M))
by NAT_1:43;
P c= Seg (len M)
by A1, A2, Th67;
then
card P <= card (Seg (len M))
by NAT_1:43;
hence
( card P <= len M & card Q <= width M )
by A3, FINSEQ_1:57; verum