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) . (- 1),f as Element of PFuncs A,REAL ;
set h = (addpfunc A) . f,g;
dom (RealPFuncZero A) = A by FUNCOP_1:19;
then dom ((RealPFuncZero A) | (dom f)) = A /\ (dom f) by RELAT_1:90;
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

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:13
.= ((RealPFuncZero A) | (dom f)) . x by A3, FUNCT_1:72 ; :: thesis: verum

end;

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