for F, G being FinSequence of INT
for v being Integer st len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) holds
Sum F = (Sum G) + v