:: deftheorem defines 0_. POLYNOM3:def 7 :
for L being non empty ZeroStr holds 0_. L = NAT --> (0. L);