theorem Th6: :: LPSPACE1:6

for A being non empty set
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) ) ) )