theorem :: FVSUM_1:17

for K being non empty addLoopStr
for p1, p2 being FinSequence of the carrier of K
for a1, a2 being Element of K
for i being Nat st i in dom (p1 + p2) & a1 = p1 . i & a2 = p2 . i holds
(p1 + p2) . i = a1 + a2 by FUNCOP_1:22;