:: deftheorem defines support BAGORD_2:def 1 :
for m being natural-valued Function holds support m = m " (NAT \ {0});