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:13;
then A1: dom ((addpfunc A) . ((RealPFuncZero A),f)) = dom f by XBOOLE_1:28;

now :: thesis: for x being Element of A st x in dom f holds
((addpfunc A) . ((RealPFuncZero A),f)) . x = f . x

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:7;
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:5; :: thesis: verum