let A be non empty set ; :: thesis: for h, f, g being Element of PFuncs A,REAL holds
( h = (addpfunc A) . f,g iff ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x) ) ) )
let h, f, g be Element of PFuncs A,REAL ; :: thesis: ( h = (addpfunc A) . f,g iff ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x) ) ) )

hereby :: thesis: ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x) ) implies h = (addpfunc A) . f,g )

assume A1: h = (addpfunc A) . f,g ; :: thesis: ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x) ) )
then dom h = dom (f + g) by RFUNCT_3:def 4;
hence dom h = (dom f) /\ (dom g) by VALUED_1:def 1; :: thesis: for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x)
let x be Element of A; :: thesis: ( x in dom h implies h . x = (f . x) + (g . x) )
assume x in dom h ; :: thesis: h . x = (f . x) + (g . x)
then ( x in dom (f + g) & h . x = (f + g) . x ) by A1, RFUNCT_3:def 4;
hence h . x = (f . x) + (g . x) by VALUED_1:def 1; :: thesis: verum

end;

assume A6: ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x) ) ) ; :: thesis: h = (addpfunc A) . f,g
set k = (addpfunc A) . f,g;

A7: now

let x be Element of A; :: thesis: ( x in dom h implies ((addpfunc A) . f,g) . x = h . x )
assume A8: x in dom h ; :: thesis: ((addpfunc A) . f,g) . x = h . x
then A10: x in dom (f + g) by A6, VALUED_1:def 1;
((addpfunc A) . f,g) . x = (f + g) . x by RFUNCT_3:def 4;
hence ((addpfunc A) . f,g) . x = (f . x) + (g . x) by A10, VALUED_1:def 1
.= h . x by A6, A8 ;
:: thesis: verum

end;

dom ((addpfunc A) . f,g) = dom (f + g) by RFUNCT_3:def 4
.= dom h by A6, VALUED_1:def 1 ;
hence h = (addpfunc A) . f,g by A7, PARTFUN1:34; :: thesis: verum