theorem ThEXP0: :: NUMBER18:6

EXP 0 = NAT --> 1