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