let n be Nat; :: thesis: ReciProducts n c= ReciProducts (n + 1)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ReciProducts n or x in ReciProducts (n + 1) )
n <= n + 1 by NAT_1:13;
then A0: SetPrimes n c= SetPrimes (n + 1) by XBOOLE_1:26, FINSEQ_1:5;
assume x in ReciProducts n ; :: thesis: x in ReciProducts (n + 1)
then consider X being Subset of (SetPrimes n) such that
A1: x = 1 / (Product (Sgm X)) ;
X c= SetPrimes (n + 1) by A0;
hence x in ReciProducts (n + 1) by A1; :: thesis: verum