let f be FinSequence of INT ; :: thesis: ex f1, f2 being FinSequence of NAT st f = f1 - f2
reconsider f1 = delneg f as FinSequence of NAT by NEWTON02:103;
reconsider f2 = delpos f as FinSequence of NAT by NEWTON02:103;
f = f1 - f2 by DNP;
hence ex f1, f2 being FinSequence of NAT st f = f1 - f2 ; :: thesis: verum