:: deftheorem defines diffield FVSUM_1:def 2 :
for K being non empty addLoopStr holds diffield K = the addF of K * ((id the carrier of K),(comp K));