let M be non empty multLoopStr ; :: thesis: ( M is well-unital implies 1. M = the_unity_wrt the multF of M )
assume H₃(M) is_a_unity_wrt the multF of M ; :: according to MONOID_0:def 21 :: thesis: 1. M = the_unity_wrt the multF of M
hence 1. M = the_unity_wrt the multF of M by BINOP_1:def 8; :: thesis: verum