theorem :: HILB10_4:22

for x, y, x1 being Nat st x1 = 0 holds
( y = Product (1 + (x1 * (idseq x))) iff y = 1 )