let D be non empty set ; :: thesis:
set F = ([#] D) --> (In (0,REAL));
A1: dom (([#] D) --> (In (0,REAL))) = D by FUNCOP_1:13;

A2: now :: thesis:

let G be Element of PFuncs (D,REAL); :: thesis:

A3: now :: thesis:

let d be Element of D; :: thesis:
assume d in dom (G + (([#] D) --> (In (0,REAL)))) ; :: thesis:
hence (G + (([#] D) --> (In (0,REAL)))) . d = (G . d) + ((([#] D) --> (In (0,REAL))) . d) by VALUED_1:def 1
.= (G . d) + 0 by FUNCOP_1:7
.= G . d ;
:: thesis:

end;

(dom G) /\ D = dom G by XBOOLE_1:28;
then dom (G + (([#] D) --> (In (0,REAL)))) = dom G by A1, VALUED_1:def 1;
then G + (([#] D) --> (In (0,REAL))) = G by A3, PARTFUN1:5;
hence (addpfunc D) . (G,(([#] D) --> (In (0,REAL)))) = G by Def4; :: thesis:

end;

addpfunc D is commutative by Th14;
hence ([#] D) --> 0 is_a_unity_wrt addpfunc D by A2, BINOP_1:5; :: thesis: