theorem Th38: :: RLVECT_1:38

for V being non empty addLoopStr
for v being Element of V
for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) holds
Sum F = (Sum G) + v