theorem Th4: :: FVSUM_1:4

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