{ (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 0) : verum } = {1}

proof

T1: { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 0) : verum } c= {1}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 0) : verum } or x in {1} )
assume x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 0) : verum } ; :: thesis: x in {1}
then consider X being Subset of (SetPrimes 0) such that
C1: x = 1 / (Product (Sgm X)) ;
Sgm X = {} by FINSEQ_3:43;
hence x in {1} by TARSKI:def 1, C1, RVSUM_1:94; :: thesis: verum

end;

{1} c= { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 0) : verum }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 0) : verum } )
assume x in {1} ; :: thesis: x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 0) : verum }
then S1: x = 1 / (Product (Sgm {})) by FINSEQ_3:43, RVSUM_1:94, TARSKI:def 1;
{} c= SetPrimes 0 ;
hence x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 0) : verum } by S1; :: thesis: verum

end;

hence { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 0) : verum } = {1} by T1, TARSKI:2; :: thesis: verum

end;

hence ReciProducts 0 = {1} ; :: thesis: verum