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 )
A3: ( Seg n = {} iff Seg m = {} ) by A2;
A4: rng nt is without_zero

proof

assume A5: 0 in rng nt ; :: according to PSCOMP_1:def 1 :: thesis: contradiction
then consider x being set such that
A6: ( x in dom nt & nt . x = 0 ) by FUNCT_1:def 5;
( dom nt = Seg n & dom mt = Seg m ) by FINSEQ_2:144;
then ( rng mt <> {} & dom M = Seg (len M) ) by A3, A6, FINSEQ_1:def 3, RELAT_1:65;
then ( [:(rng nt),(rng mt):] <> {} & Indices M = [:(Seg (len M)),(Seg (width M)):] ) by A5;
then rng nt c= Seg (len M) by A1, ZFMISC_1:138;
hence contradiction by A5; :: thesis: verum

end;

rng mt is without_zero

proof

assume A7: 0 in rng mt ; :: according to PSCOMP_1:def 1 :: thesis: contradiction
then consider x being set such that
A8: ( x in dom mt & mt . x = 0 ) by FUNCT_1:def 5;
( dom nt = Seg n & dom mt = Seg m ) by FINSEQ_2:144;
then ( rng nt <> {} & dom M = Seg (len M) ) by A3, A8, FINSEQ_1:def 3, RELAT_1:65;
then ( [:(rng nt),(rng mt):] <> {} & Indices M = [:(Seg (len M)),(Seg (width M)):] ) by A7;
then rng mt c= Seg (width M) by A1, ZFMISC_1:138;
hence contradiction by A7; :: thesis: verum

end;

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