theorem :: POLYDIFF:8

#Z 0 = REAL --> 1