let D be non empty set ; :: thesis: addpfunc D is having_a_unity
take ([#] D) --> 0 ; :: according to SETWISEO:def 2 :: thesis: ([#] D) --> 0 is_a_unity_wrt addpfunc D
thus ([#] D) --> 0 is_a_unity_wrt addpfunc D by Th18; :: thesis: verum