Sgm {2} = <*2*> by FINSEQ_3:44;
then A2: 1 / (Product (Sgm {2})) = 1 / 2 by RVSUM_1:95;
{2} c= SetPrimes 2 by Set2;
then S1: 1 / 2 in ReciProducts 2 by A2;
{} c= Seg 1 ;
then A4: Product (Sgm {}) = 1 by RVSUM_1:94, FINSEQ_1:51;
Z1: {} c= SetPrimes 2 ;
1 / (Product (Sgm {})) = 1 by A4;
then 1 in ReciProducts 2 by Z1;
then ZZ: {(1 / 2),1} c= ReciProducts 2 by ZFMISC_1:32, S1;
ReciProducts 2 c= {(1 / 2),1}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ReciProducts 2 or x in {(1 / 2),1} )
assume x in ReciProducts 2 ; :: thesis: x in {(1 / 2),1}
then consider X being Subset of (SetPrimes 2) such that
N1: x = 1 / (Product (Sgm X)) ;
( X = {} or X = {2} ) by ZFMISC_1:33, Set2;
hence x in {(1 / 2),1} by TARSKI:def 2, N1, A4, A2; :: thesis: verum
end;
hence ReciProducts 2 = {(1 / 2),1} by TARSKI:2, ZZ; :: thesis: verum