:: deftheorem defines delall FINSEQ_9:def 3 :
for f being complex-valued Function holds delall f = 0 (#) f;