let f1, f2, g be PartFunc of REAL ,REAL ; :: thesis: for A being 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)|||
let A be closed-interval Subset of REAL ; :: thesis: ( (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 implies |||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)||| )
assume A1: ( (f1 (#) g) || A is total & (f2 (#) g) || A is total ) ; :: thesis: ( not ((f1 (#) g) || A) | A is bounded or not (f1 (#) g) || A is integrable or not ((f2 (#) g) || A) | A is bounded or not (f2 (#) g) || A is integrable or |||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)||| )
assume A2: ( ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable ) ; :: thesis: |||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)|||
|||((f1 + f2),g,A)||| = integral (((f1 + f2) || A) (#) (g || A)) by INTEGRA5:4
.= integral (((f1 (#) g) + (f2 (#) g)) || A) by Th27
.= integral (((f1 (#) g) || A) + ((f2 (#) g) || A)) by INTEGRA5:5
.= (integral ((f1 (#) g) || A)) + (integral ((f2 (#) g) || A)) by A1, A2, INTEGRA1:59 ;
hence |||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)||| ; :: thesis: verum