for f1, f2, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f1 (#) g) || A is total & (f2 (#) g) || A is total & ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable holds
|||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)|||