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

A2: now :: thesis: for G being Element of PFuncs (D,REAL) holds (addpfunc D) . (G,(([#] D) --> (In (0,REAL)))) = G

let G be Element of PFuncs (D,REAL); :: thesis: (addpfunc D) . (G,(([#] D) --> (In (0,REAL)))) = G

A3: now :: thesis: for d being Element of D st d in dom (G + (([#] D) --> (In (0,REAL)))) holds
(G + (([#] D) --> (In (0,REAL)))) . d = G . d

let d be Element of D; :: thesis: ( d in dom (G + (([#] D) --> (In (0,REAL)))) implies (G + (([#] D) --> (In (0,REAL)))) . d = G . d )
assume d in dom (G + (([#] D) --> (In (0,REAL)))) ; :: thesis: (G + (([#] D) --> (In (0,REAL)))) . d = G . d
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: verum

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: verum

end;

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