let K be non empty left_zeroed right_zeroed addLoopStr ; :: thesis: the_unity_wrt the addF of K = 0. K
reconsider e = 0. K as Element of K ;
e is_a_unity_wrt the addF of K by Th6;
hence the_unity_wrt the addF of K = 0. K by BINOP_1:def 8; :: thesis: verum