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