let D be non empty set ; :: thesis: the_unity_wrt (addpfunc D) = ([#] D) --> 0
([#] D) --> (In (0,REAL)) is_a_unity_wrt addpfunc D by Th16;
hence the_unity_wrt (addpfunc D) = ([#] D) --> 0 by BINOP_1:def 8; :: thesis: verum