let K be non empty left_zeroed right_zeroed addLoopStr ; :: thesis: the addF of K is having_a_unity
take 0. K ; :: according to SETWISEO:def 2 :: thesis: 0. K is_a_unity_wrt the addF of K
thus 0. K is_a_unity_wrt the addF of K by Th6; :: thesis: verum