theorem Th4: :: LPSPACC1:4

for A being non empty set
for f, g, h being Element of PFuncs (A,COMPLEX) holds
( h = (addcpfunc 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) ) ) )