let p be Prime; :: thesis: for n being Element of NAT
for m being non zero Element of NAT
for X being set st X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P₁[n,m,p9] } & not p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = 0
let n be Element of NAT ; :: thesis: for m being non zero Element of NAT
for X being set st X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P₁[n,m,p9] } & not p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = 0
let m be non zero Element of NAT ; :: thesis: for X being set st X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P₁[n,m,p9] } & not p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = 0
let X be set ; :: thesis: ( X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P₁[n,m,p9] } & not p |^ (p |-count m) in X implies p |-count (Product (Sgm X)) = 0 )
assume A1: X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P₁[n,m,p9] } ; :: thesis: ( p |^ (p |-count m) in X or p |-count (Product (Sgm X)) = 0 )
set f = p |-count (Sgm X);
set g = (len (p |-count (Sgm X))) |-> 0;
assume A2: not p |^ (p |-count m) in X ; :: thesis: p |-count (Product (Sgm X)) = 0
A3: for k being Nat st 1 <= k & k <= len (p |-count (Sgm X)) holds
(p |-count (Sgm X)) . k = ((len (p |-count (Sgm X))) |-> 0) . k

proof

set XX = Seg m;
let k be Nat; :: thesis: ( 1 <= k & k <= len (p |-count (Sgm X)) implies (p |-count (Sgm X)) . k = ((len (p |-count (Sgm X))) |-> 0) . k )
assume A4: 1 <= k ; :: thesis: ( not k <= len (p |-count (Sgm X)) or (p |-count (Sgm X)) . k = ((len (p |-count (Sgm X))) |-> 0) . k )
assume k <= len (p |-count (Sgm X)) ; :: thesis: (p |-count (Sgm X)) . k = ((len (p |-count (Sgm X))) |-> 0) . k
then A5: k in Seg (len (p |-count (Sgm X))) by A4, FINSEQ_1:1;
then k in dom (p |-count (Sgm X)) by FINSEQ_1:def 3;
then A6: (p |-count (Sgm X)) . k = p |-count ((Sgm X) . k) by Def1;

now :: thesis: for x being object st x in X holds
x in Seg m

let x be object ; :: thesis: ( x in X implies x in Seg m )
assume x in X ; :: thesis: x in Seg m
then consider y9 being prime Element of NAT such that
B1: ( y9 |^ (y9 |-count m) = x & P₁[n,m,y9] ) by A1;
( 1 <= y9 |^ (y9 |-count m) & y9 |^ (y9 |-count m) <= m ) by Th16;
hence x in Seg m by B1, FINSEQ_1:1; :: thesis: verum

end;

then X c= Seg m ;
then X is included_in_Seg by FINSEQ_1:def 13;
then A7: rng (Sgm X) = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P₁[n,m,p9] } by A1, FINSEQ_1:def 14;
len (p |-count (Sgm X)) = len (Sgm X) by Def1;
then k in dom (Sgm X) by A5, FINSEQ_1:def 3;
then (Sgm X) . k in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P₁[n,m,p9] } by A7, FUNCT_1:3;
then consider p1 being prime Element of NAT such that
A8: p1 |^ (p1 |-count m) = (Sgm X) . k and
A9: P₁[n,m,p1] ;
p1 <> p by A1, A2, A9;
then ( p <> 1 & not p divides p1 |^ (p1 |-count m) ) by INT_2:def 4, NAT_3:6;
then (p |-count (Sgm X)) . k = 0 by A6, A8, NAT_3:27;
hence (p |-count (Sgm X)) . k = ((len (p |-count (Sgm X))) |-> 0) . k ; :: thesis: verum

end;

for p being Prime
for n being Element of NAT
for m being non zero Element of NAT
for X being set st X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P₁[n,m,p9] } holds
Product (Sgm X) > 0 from NAT_4:sch 1();
then Product (Sgm X) <> 0 by A1;
then A10: p |-count (Product (Sgm X)) = Sum (p |-count (Sgm X)) by Th52;
( len (p |-count (Sgm X)) = len ((len (p |-count (Sgm X))) |-> 0) & Sum ((len (p |-count (Sgm X))) |-> 0) = (len (p |-count (Sgm X))) * 0 ) by CARD_1:def 7, RVSUM_1:80;
hence p |-count (Product (Sgm X)) = 0 by A10, A3, FINSEQ_1:14; :: thesis: verum