theorem Th12: :: FVSUM_1:12

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;