let m, n 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 2 :: thesis: contradiction
rng mt <> {} by A2, A4;
then rng nt c= Seg (len M) by A1, A3, ZFMISC_1:114;
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 2 :: thesis: contradiction
rng nt <> {} by A2, A6;
then rng mt c= Seg (width M) by A1, ZFMISC_1:114;
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