theorem :: FVSUM_1:9

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