set Y = ReciProducts n;
deffunc H1( Subset of (SetPrimes n)) -> set = 1 / (Product (Sgm n));
A3: ReciProducts n c= { H1(X) where X is Element of bool (SetPrimes n) : X in bool (SetPrimes n) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ReciProducts n or x in { H1(X) where X is Element of bool (SetPrimes n) : X in bool (SetPrimes n) } )
assume x in ReciProducts n ; :: thesis: x in { H1(X) where X is Element of bool (SetPrimes n) : X in bool (SetPrimes n) }
then consider X being Subset of (SetPrimes n) such that
B1: x = 1 / (Product (Sgm X)) ;
thus x in { H1(X) where X is Element of bool (SetPrimes n) : X in bool (SetPrimes n) } by B1; :: thesis: verum
end;
A1: bool (SetPrimes n) is finite ;
{ H1(w) where w is Element of bool (SetPrimes n) : w in bool (SetPrimes n) } is finite from FRAENKEL:sch 21(A1);
 hence ReciProducts n is finite by A3; :: thesis: verum