let A be non empty set ; :: thesis: for f, g, h 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 f, g, h 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 A2: x in dom (f + g) by A1, RFUNCT_3:def 4;
h . x = (f + g) . x by A1, RFUNCT_3:def 4;
hence h . x = (f . x) + (g . x) by A2, VALUED_1:def 1; :: thesis: verum

end;

assume that
A3: dom h = (dom f) /\ (dom g) and
A4: 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);

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

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

end;

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