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'] } holds
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'] } holds
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'] } holds
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'] } implies Product (Sgm X) > 0 )
set f = Sgm X;
assume A1: X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P₁[n,m,p'] } ; :: 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

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 A3: rng (Sgm X) = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P₁[n,m,p'] } by A1, FINSEQ_1:def 13;
assume k in dom (Sgm X) ; :: thesis: (Sgm X) . k > 0
then (Sgm X) . k in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P₁[n,m,p'] } by A3, FUNCT_1:12;
then ex y' being prime Element of NAT st
( y' |^ (y' |-count m) = (Sgm X) . k & P₁[n,m,y'] ) ;
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, Th42; :: thesis: verum