let A be non empty set ; :: thesis: for f being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,((multrealpfunc A) . ((- 1),f))) = (RealPFuncZero A) | (dom f)
let f be Element of PFuncs (A,REAL); :: thesis: (addpfunc A) . (f,((multrealpfunc A) . ((- 1),f))) = (RealPFuncZero A) | (dom f)
reconsider g = (multrealpfunc A) . ((- jj),f) as Element of PFuncs (A,REAL) ;
set h = (addpfunc A) . (f,g);
dom (RealPFuncZero A) = A by FUNCOP_1:13;
then dom ((RealPFuncZero A) | (dom f)) = A /\ (dom f) by RELAT_1:61;
then A1: dom ((RealPFuncZero A) | (dom f)) = dom f by XBOOLE_1:28;
A2: dom ((addpfunc A) . (f,g)) = (dom g) /\ (dom f) by Th6
.= (dom f) /\ (dom f) by Th9 ;

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

let x be Element of A; :: thesis: ( x in dom f implies ((addpfunc A) . (f,g)) . x = ((RealPFuncZero A) | (dom f)) . x )
assume A3: x in dom f ; :: thesis: ((addpfunc A) . (f,g)) . x = ((RealPFuncZero A) | (dom f)) . x
then A4: x in dom ((- 1) (#) f) by VALUED_1:def 5;
thus ((addpfunc A) . (f,g)) . x = (f . x) + (g . x) by A2, A3, Th6
.= (f . x) + (((- 1) (#) f) . x) by Def4
.= (f . x) + ((- 1) * (f . x)) by A4, VALUED_1:def 5
.= (RealPFuncZero A) . x by FUNCOP_1:7
.= ((RealPFuncZero A) | (dom f)) . x by A3, FUNCT_1:49 ; :: thesis: verum

end;

hence (addpfunc A) . (f,((multrealpfunc A) . ((- 1),f))) = (RealPFuncZero A) | (dom f) by A1, A2, PARTFUN1:5; :: thesis: verum