theorem :: FINSEQ_9:29
for f being FinSequence of INT ex f1, f2 being FinSequence of NAT st f = f1 - f2