let A be non empty set ; :: thesis: for f being Element of PFuncs A,REAL holds (addpfunc A) . (RealPFuncZero A),f = f
let f be Element of PFuncs A,REAL ; :: thesis: (addpfunc A) . (RealPFuncZero A),f = f
set h = (addpfunc A) . (RealPFuncZero A),f;
dom ((addpfunc A) . (RealPFuncZero A),f) = (dom (RealPFuncZero A)) /\ (dom f) by Th6;
then dom ((addpfunc A) . (RealPFuncZero A),f) = A /\ (dom f) by FUNCOP_1:19;
then A1: dom ((addpfunc A) . (RealPFuncZero A),f) = dom f by XBOOLE_1:28;

now

let x be Element of A; :: thesis: ( x in dom f implies ((addpfunc A) . (RealPFuncZero A),f) . x = f . x )
A2: (RealPFuncZero A) . x = 0 by FUNCOP_1:13;
assume x in dom f ; :: thesis: ((addpfunc A) . (RealPFuncZero A),f) . x = f . x
hence ((addpfunc A) . (RealPFuncZero A),f) . x = 0 + (f . x) by A1, A2, Th6
.= f . x ;
:: thesis: verum

end;

hence (addpfunc A) . (RealPFuncZero A),f = f by A1, PARTFUN1:34; :: thesis: verum