theorem Th20:
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 ) )