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

A2: now

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

A3: now

let d be Element of D; :: thesis: ( d in dom (G + (([#] D) --> 0)) implies (G + (([#] D) --> 0)) . d = G . d )
assume d in dom (G + (([#] D) --> 0)) ; :: thesis: (G + (([#] D) --> 0)) . d = G . d
hence (G + (([#] D) --> 0)) . d = (G . d) + ((([#] D) --> 0) . 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) --> 0)) = dom G by A1, VALUED_1:def 1;
then G + (([#] D) --> 0) = G by A3, PARTFUN1:5;
hence (addpfunc D) . (G,(([#] D) --> 0)) = G by Def4; :: thesis: verum

end;

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