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:19;

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:13
.= 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:34;
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:13; :: thesis: verum