:: deftheorem defines + FVSUM_1:def 3 :
for K being non empty addLoopStr
for p1, p2 being FinSequence of the carrier of K holds p1 + p2 = the addF of K .: (p1,p2);