let p be Prime; :: thesis: for n being Element of NAT
for m being non empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P₁[n,m,p'] } & 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 empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P₁[n,m,p'] } & not p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = 0
let m be non empty Element of NAT ; :: thesis: for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P₁[n,m,p'] } & not p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = 0
let X be set ; :: thesis: ( X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P₁[n,m,p'] } & not p |^ (p |-count m) in X implies p |-count (Product (Sgm X)) = 0 )
assume A1: X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P₁[n,m,p'] } ; :: thesis: ( p |^ (p |-count m) in X or p |-count (Product (Sgm X)) = 0 )
assume A2: not p |^ (p |-count m) in X ; :: thesis: p |-count (Product (Sgm X)) = 0
for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P₁[n,m,p'] } holds
Product (Sgm X) > 0 from NAT_4:sch 1();
then Product (Sgm X) <> 0 by A1;
then A3: p |-count (Product (Sgm X)) = Sum (p |-count (Sgm X)) by Th53;
set f = p |-count (Sgm X);
set g = (len (p |-count (Sgm X))) |-> 0 ;
A4: len (p |-count (Sgm X)) = len ((len (p |-count (Sgm X))) |-> 0 ) by FINSEQ_1:def 18;
A5: 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

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 A6: 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 A7: k in Seg (len (p |-count (Sgm X))) by A6, FINSEQ_1:3;
then k in dom (p |-count (Sgm X)) by FINSEQ_1:def 3;
then A8: ( (p |-count (Sgm X)) . k = p |-count ((Sgm X) . k) & len (p |-count (Sgm X)) = len (Sgm X) ) by Def1;
set XX = Seg m;

now

let x be set ; :: thesis: ( x in X implies x in Seg m )
assume x in X ; :: thesis: x in Seg m
then ex y' being prime Element of NAT st
( y' |^ (y' |-count m) = x & P₁[n,m,y'] ) by A1;
then ex b being Element of NAT st
( b = x & 1 <= b & b <= m ) by Th16;
hence x in Seg m by FINSEQ_1:3; :: thesis: verum

end;

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

end;

Sum ((len (p |-count (Sgm X))) |-> 0 ) = (len (p |-count (Sgm X))) * 0 by RVSUM_1:110;
hence p |-count (Product (Sgm X)) = 0 by A3, A4, A5, FINSEQ_1:18; :: thesis: verum