for x, y, x1 being Nat st x1 >= 1 holds
( y = Product (1 + (x1 * (idseq x))) iff ex u, w, y1, y2, y3, y4, y5 being Nat st
( u > y & x1 * w,1 are_congruent_mod u & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod u & y4 = 1 + (x1 * x) & y5 = y4 |^ x & u > y5 ) )