let f1, f2, g be PartFunc of REAL,REAL; :: thesis: 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)|||
let A be non empty 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 Th22
.= integral (((f1 (#) g) || A) - ((f2 (#) g) || A)) by Th20
.= (integral ((f1 (#) g) || A)) - (integral ((f2 (#) g) || A)) by A1, A2, INTEGRA2:33 ;
hence |||((f1 - f2),g,A)||| = |||(f1,g,A)||| - |||(f2,g,A)||| ; :: thesis: verum