theorem :: POLYDIFF:8
#Z 0 = REAL --> 1