theorem :: WSIERP_1:20

for a being Nat
for ft being FinSequence of REAL st a in dom ft holds
(Sum (Del (ft,a))) + (ft . a) = Sum ft