theorem :: FINSEQ_9:19

for f being complex-valued FinSequence holds
( f - f = 0 (#) f & f - f = (len f) |-> 0 )