for K being non empty distributive doubleLoopStr
for a being Element of K holds a multfield is_distributive_wrt the addF of K by Th10, FINSEQOP:54;