for K being non empty commutative left_unital multLoopStr holds 1. K is_a_unity_wrt the multF of K