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] } holds
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] } holds
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] } holds
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] } implies Product (Sgm X) > 0 )
set f = Sgm X;
assume A1: X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P₁[n,m,p9] } ; :: thesis: Product (Sgm X) > 0
A2: for k being Element of NAT st k in dom (Sgm X) holds
(Sgm X) . k > 0

proof

set XX = Seg m;
let k be Element of NAT ; :: thesis: ( k in dom (Sgm X) implies (Sgm X) . k > 0 )

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
A4: ( 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 A4, FINSEQ_1:1; :: thesis: verum

end;

then X c= Seg m ;
then X is included_in_Seg by FINSEQ_1:def 13;
then A3: rng (Sgm X) = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P₁[n,m,p9] } by A1, FINSEQ_1:def 14;
assume k in dom (Sgm X) ; :: thesis: (Sgm X) . k > 0
then (Sgm X) . k in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P₁[n,m,p9] } by A3, FUNCT_1:3;
then ex y9 being prime Element of NAT st
( y9 |^ (y9 |-count m) = (Sgm X) . k & P₁[n,m,y9] ) ;
hence (Sgm X) . k > 0 ; :: thesis: verum

end;

rng (Sgm X) c= REAL ;
then Sgm X is FinSequence of REAL by FINSEQ_1:def 4;
hence Product (Sgm X) > 0 by A2, Th41; :: thesis: verum