let n, m be Nat; :: thesis: for K being Field
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K holds
not ( [:(rng nt),(rng mt):] c= Indices M & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & ( for P1, P2 being finite without_zero Subset of NAT holds
( not P1 = rng nt or not P2 = rng mt ) ) )
let K be Field; :: thesis: for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K holds
not ( [:(rng nt),(rng mt):] c= Indices M & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & ( for P1, P2 being finite without_zero Subset of NAT holds
( not P1 = rng nt or not P2 = rng mt ) ) )
let nt be Element of n -tuples_on NAT ; :: thesis: for mt being Element of m -tuples_on NAT
for M being Matrix of K holds
not ( [:(rng nt),(rng mt):] c= Indices M & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & ( for P1, P2 being finite without_zero Subset of NAT holds
( not P1 = rng nt or not P2 = rng mt ) ) )
let mt be Element of m -tuples_on NAT ; :: thesis: for M being Matrix of K holds
not ( [:(rng nt),(rng mt):] c= Indices M & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & ( for P1, P2 being finite without_zero Subset of NAT holds
( not P1 = rng nt or not P2 = rng mt ) ) )
let M be Matrix of K; :: thesis: not ( [:(rng nt),(rng mt):] c= Indices M & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & ( for P1, P2 being finite without_zero Subset of NAT holds
( not P1 = rng nt or not P2 = rng mt ) ) )
assume that
A1: [:(rng nt),(rng mt):] c= Indices M and
A2: ( n = 0 iff m = 0 ) ; :: thesis: ex P1, P2 being finite without_zero Subset of NAT st
( P1 = rng nt & P2 = rng mt )
rng nt is without_zero

proof

A3: Indices M = [:(Seg (len M)),(Seg (width M)):] by FINSEQ_1:def 3;
assume A4: 0 in rng nt ; :: according to MEASURE6:def 6 :: thesis: contradiction
dom mt = Seg m by FINSEQ_2:144;
then rng mt <> {} by A2, A4, RELAT_1:65;
then rng nt c= Seg (len M) by A1, A4, A3, ZFMISC_1:138;
hence contradiction by A4; :: thesis: verum

end;

then A5: rng nt is finite without_zero Subset of NAT by FINSEQ_1:def 4;
rng mt is without_zero

proof

assume A6: 0 in rng mt ; :: according to MEASURE6:def 6 :: thesis: contradiction
dom nt = Seg n by FINSEQ_2:144;
then rng nt <> {} by A2, A6, RELAT_1:65;
then rng mt c= Seg (width M) by A1, A6, ZFMISC_1:138;
hence contradiction by A6; :: thesis: verum

end;

then rng mt is finite without_zero Subset of NAT by FINSEQ_1:def 4;
hence ex P1, P2 being finite without_zero Subset of NAT st
( P1 = rng nt & P2 = rng mt ) by A5; :: thesis: verum