theorem :: FVSUM_1:19

for K being non empty addLoopStr
for a1, a2 being Element of K holds <*a1*> + <*a2*> = <*(a1 + a2)*> by FINSEQ_2:74;