:: deftheorem defines 0c SEQ_4:def 12 :
for n being Nat holds 0c n = n |-> 0c;