theorem :: FVSUM_1:34

for K being non empty addLoopStr
for a1, a2 being Element of K holds <*a1*> - <*a2*> = <*(a1 - a2)*>