for K being non empty commutative left_unital multLoopStr holds the multF of K is having_a_unity ;