{ (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 1) : verum } = {1}
proof
T1: { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 1) : 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 1) : verum } or x in {1} )
assume x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 1) : verum } ; :: thesis: x in {1}
then consider X being Subset of (SetPrimes 1) such that
C1: x = 1 / (Product (Sgm X)) ;
Sgm X = {} by FINSEQ_3:43, SetPrime1;
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 1) : 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 1) : verum } )
assume x in {1} ; :: thesis: x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 1) : verum }
then S1: x = 1 / (Product (Sgm {})) by FINSEQ_3:43, RVSUM_1:94, TARSKI:def 1;
{} c= SetPrimes 1 ;
hence x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 1) : verum } by S1; :: thesis: verum
end;
hence { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes 1) : verum } = {1} by T1, TARSKI:2; :: thesis: verum
end;
hence ReciProducts 1 = {1} ; :: thesis: verum