let K be non empty commutative left_unital multLoopStr ; :: thesis: the multF of K is having_a_unity
take 1. K ; :: according to SETWISEO:def 2 :: thesis: 1. K is_a_unity_wrt the multF of K
thus 1. K is_a_unity_wrt the multF of K by Th6; :: thesis: verum