theorem Th10: :: FVSUM_1:10

for K being non empty distributive doubleLoopStr holds the multF of K is_distributive_wrt the addF of K