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