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