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] } & p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = p |-count m
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] } & p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = p |-count m
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] } & p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = p |-count m
let X be set ; :: thesis: ( X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P₁[n,m,p9] } & p |^ (p |-count m) in X implies p |-count (Product (Sgm X)) = p |-count m )
set XX = Seg m;
defpred S₁[ Element of NAT , Element of NAT , Prime] means ( P₁[$1,$2,$3] & $3 |^ ($3 |-count $2) <= p |^ (p |-count $2) );
defpred S₂[ Element of NAT , Element of NAT , Prime] means ( P₁[$1,$2,$3] & $3 |^ ($3 |-count $2) > p |^ (p |-count $2) );
set X1 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } ;
set X2 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } ;

A1: now :: thesis: for k1, k2 being Nat st k1 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } & k2 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } holds
k1 < k2

let k1, k2 be Nat; :: thesis: ( k1 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } & k2 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } implies k1 < k2 )
assume ( k1 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } & k2 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } ) ; :: thesis: k1 < k2
then ( ex p1 being prime Element of NAT st
( p1 |^ (p1 |-count m) = k1 & S₁[n,m,p1] ) & ex p2 being prime Element of NAT st
( p2 |^ (p2 |-count m) = k2 & S₂[n,m,p2] ) ) ;
hence k1 < k2 by XXREAL_0:2; :: thesis: verum

end;

A2: now :: thesis: not p |^ (p |-count m) in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] }

assume p |^ (p |-count m) in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } ; :: thesis: contradiction
then ex p9 being prime Element of NAT st
( p9 |^ (p9 |-count m) = p |^ (p |-count m) & S₂[n,m,p9] ) ;
hence contradiction ; :: thesis: verum

end;

set m1 = p |^ (p |-count m);
defpred S₃[ Element of NAT , Element of NAT , Prime] means ( P₁[$1,$2,$3] & $3 |^ ($3 |-count $2) = p |^ (p |-count $2) );
defpred S₄[ Element of NAT , Element of NAT , Prime] means ( P₁[$1,$2,$3] & $3 |^ ($3 |-count $2) < p |^ (p |-count $2) );
set X11 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } ;
set X12 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } ;

A3: now :: thesis: for k1, k2 being Nat st k1 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } & k2 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } holds
k1 < k2

let k1, k2 be Nat; :: thesis: ( k1 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } & k2 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } implies k1 < k2 )
assume ( k1 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } & k2 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } ) ; :: thesis: k1 < k2
then ( ex p1 being prime Element of NAT st
( p1 |^ (p1 |-count m) = k1 & S₄[n,m,p1] ) & ex p2 being prime Element of NAT st
( p2 |^ (p2 |-count m) = k2 & S₃[n,m,p2] ) ) ;
hence k1 < k2 ; :: thesis: verum

end;

now :: thesis: for x being object st x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } holds
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] }

let x be object ; :: thesis: ( x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } implies x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } )
assume x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } ; :: thesis: x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] }
then consider p9 being prime Element of NAT such that
A4: ( p9 |^ (p9 |-count m) = x & S₁[n,m,p9] ) ;
( ( p9 |^ (p9 |-count m) = x & S₄[n,m,p9] ) or ( p9 |^ (p9 |-count m) = x & S₃[n,m,p9] ) ) by A4, XXREAL_0:1;
then ( x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } or x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } ) ;
hence x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } by XBOOLE_0:def 3; :: thesis: verum

end;

then A5: { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } c= { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } ;
assume A6: X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P₁[n,m,p9] } ; :: thesis: ( not p |^ (p |-count m) in X or p |-count (Product (Sgm X)) = p |-count m )

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 A6;
( 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 A7: X c= Seg m ;

now :: thesis: for x being object st x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } holds
x in {(p |^ (p |-count m))}

let x be object ; :: thesis: ( x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } implies x in {(p |^ (p |-count m))} )
assume x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } ; :: thesis: x in {(p |^ (p |-count m))}
then ex p9 being prime Element of NAT st
( p9 |^ (p9 |-count m) = x & S₃[n,m,p9] ) ;
hence x in {(p |^ (p |-count m))} by TARSKI:def 1; :: thesis: verum

end;

then A8: { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } c= {(p |^ (p |-count m))} ;
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 A9: Product (Sgm X) <> 0 by A6;
A10: 1 < p by INT_2:def 4;
A11: p |-count (p |^ (p |-count m)) = (p |-count m) * (p |-count p) by NAT_3:32
.= (p |-count m) * 1 by A10, NAT_3:22 ;

now :: thesis: for x being object st x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } holds
x in X

let x be object ; :: thesis: ( x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } implies x in X )
assume x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } ; :: thesis: x in X
then ex p9 being prime Element of NAT st
( p9 |^ (p9 |-count m) = x & S₁[n,m,p9] ) ;
hence x in X by A6; :: thesis: verum

end;

then A12: { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } c= X ;
then A13: { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } c= Seg m by A7;
then a13: { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } is included_in_Seg by FINSEQ_1:def 13;

now :: thesis: for x being object st x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } holds
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] }

let x be object ; :: thesis: ( x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } implies x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } )
assume x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } ; :: thesis: x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] }
then ex p9 being prime Element of NAT st
( p9 |^ (p9 |-count m) = x & S₃[n,m,p9] ) ;
hence x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } ; :: thesis: verum

end;

then A14: { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } c= { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } ;
then { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } c= Seg m by A13;
then a15: { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } is included_in_Seg by FINSEQ_1:def 13;

now :: thesis: for x being object st x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } holds
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] }

let x be object ; :: thesis: ( x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } implies x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } )
assume x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } ; :: thesis: x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] }
then ex p9 being prime Element of NAT st
( p9 |^ (p9 |-count m) = x & S₄[n,m,p9] ) ;
hence x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } ; :: thesis: verum

end;

then A16: { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } c= { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } ;
then { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } c= Seg m by A13;
then a17: { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } is included_in_Seg by FINSEQ_1:def 13;
{ (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } c= { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } by A16, A14, XBOOLE_1:13;
then A18: Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } )) = Sum (p |-count (Sgm ( { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } ))) by A5, XBOOLE_0:def 10
.= Sum (p |-count ((Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } ) ^ (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } ))) by a17, a15, A3, FINSEQ_3:42
.= Sum ((p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } )) ^ (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } ))) by Th50
.= (Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } ))) + (Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } ))) by RVSUM_1:75 ;
for p being Prime
for n being Element of NAT
for m being non zero Element of NAT
for X2 being set st X2 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } & not p |^ (p |-count m) in X2 holds
p |-count (Product (Sgm X2)) = 0 from NAT_4:sch 2();
then A19: p |-count (Product (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } )) = 0 by A2;
for p being Prime
for n being Element of NAT
for m being non zero Element of NAT
for X2 being set st X2 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } holds
Product (Sgm X2) > 0 from NAT_4:sch 1();
then A20: Product (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } ) <> 0 ;

now :: thesis: for x being object st x in X holds
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] }

let x be object ; :: thesis: ( x in X implies x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } )
assume x in X ; :: thesis: x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] }
then consider p9 being prime Element of NAT such that
A21: ( p9 |^ (p9 |-count m) = x & P₁[n,m,p9] ) by A6;
( ( p9 |^ (p9 |-count m) = x & S₁[n,m,p9] ) or ( p9 |^ (p9 |-count m) = x & S₂[n,m,p9] ) ) by A21;
then ( x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } or x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } ) ;
hence x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } by XBOOLE_0:def 3; :: thesis: verum

end;

then A22: X c= { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } ;

now :: thesis: for x being object st x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } holds
x in X

let x be object ; :: thesis: ( x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } implies x in X )
assume x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } ; :: thesis: x in X
then ex p9 being prime Element of NAT st
( p9 |^ (p9 |-count m) = x & S₂[n,m,p9] ) ;
hence x in X by A6; :: thesis: verum

end;

then A23: { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } c= X ;
then { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } c= Seg m by A7;
then a24: { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } is included_in_Seg by FINSEQ_1:def 13;
reconsider m1 = p |^ (p |-count m) as non zero Element of NAT by ORDINAL1:def 12;

A25: now :: thesis: not p |^ (p |-count m) in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] }

assume p |^ (p |-count m) in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } ; :: thesis: contradiction
then ex p9 being prime Element of NAT st
( p9 |^ (p9 |-count m) = p |^ (p |-count m) & S₄[n,m,p9] ) ;
hence contradiction ; :: thesis: verum

end;

assume p |^ (p |-count m) in X ; :: thesis: p |-count (Product (Sgm X)) = p |-count m
then p |^ (p |-count m) in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } by A22, A2, XBOOLE_0:def 3;
then p |^ (p |-count m) in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } by A5, A25, XBOOLE_0:def 3;
then for x being object st x in {(p |^ (p |-count m))} holds
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } by TARSKI:def 1;
then A26: {(p |^ (p |-count m))} c= { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } ;
for p being Prime
for n being Element of NAT
for m being non zero Element of NAT
for X11 being set st X11 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } & not p |^ (p |-count m) in X11 holds
p |-count (Product (Sgm X11)) = 0 from NAT_4:sch 2();
then A27: p |-count (Product (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } )) = 0 by A25;
for p being Prime
for n being Element of NAT
for m being non zero Element of NAT
for X11 being set st X11 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } holds
Product (Sgm X11) > 0 from NAT_4:sch 1();
then A28: Product (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₄[n,m,p9] } ) <> 0 ;
{ (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } c= X \/ X by A12, A23, XBOOLE_1:13;
then Sum (p |-count (Sgm X)) = Sum (p |-count (Sgm ( { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } ))) by A22, XBOOLE_0:def 10
.= Sum (p |-count ((Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } ) ^ (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } ))) by a13, a24, A1, FINSEQ_3:42
.= Sum ((p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } )) ^ (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } ))) by Th50
.= (Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } ))) + (Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } ))) by RVSUM_1:75 ;
then p |-count (Product (Sgm X)) = (Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } ))) + (Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₂[n,m,p9] } ))) by A9, Th52
.= (Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₁[n,m,p9] } ))) + 0 by A20, A19, Th52
.= 0 + (Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S₃[n,m,p9] } ))) by A18, A28, A27, Th52
.= Sum (p |-count (Sgm {(p |^ (p |-count m))})) by A26, A8, XBOOLE_0:def 10
.= Sum (p |-count <*m1*>) by FINSEQ_3:44
.= Sum <*(p |-count m1)*> by Th51
.= p |-count m1 by RVSUM_1:73 ;
hence p |-count (Product (Sgm X)) = p |-count m by A11; :: thesis: verum