let G be non empty unital multMagma ; :: thesis: the multF of G is having_a_unity
take 1_ G ; :: according to SETWISEO:def 2 :: thesis: 1_ G is_a_unity_wrt the multF of G
thus 1_ G is_a_unity_wrt the multF of G by Th32; :: thesis: verum