theorem Th5: :: FVSUM_1:5

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