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 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

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