theorem Th11: :: FVSUM_1:11

for K being non empty addLoopStr
for a1, a2 being Element of K holds (diffield K) . (a1,a2) = a1 - a2