set Y = ReciProducts n;
deffunc H₁( Subset of (SetPrimes n)) -> set = 1 / (Product (Sgm n));
A3: ReciProducts n c= { H₁(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 { H₁(X) where X is Element of bool (SetPrimes n) : X in bool (SetPrimes n) } )
assume x in ReciProducts n ; :: thesis: x in { H₁(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 { H₁(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 ;
{ H₁(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