let f, g be PartFunc of REAL ,REAL ; :: thesis: for A being closed-interval Subset of REAL st (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A holds
|||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)|||
let A be closed-interval Subset of REAL ; :: thesis: ( (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A implies |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| )
assume A1: ( (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total ) ; :: thesis: ( not ((f (#) f) || A) | A is bounded or not ((f (#) g) || A) | A is bounded or not ((g (#) g) || A) | A is bounded or not f (#) f is_integrable_on A or not f (#) g is_integrable_on A or not g (#) g is_integrable_on A or |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| )
assume A2: ( ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded ) ; :: thesis: ( not f (#) f is_integrable_on A or not f (#) g is_integrable_on A or not g (#) g is_integrable_on A or |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| )
then A3: ( (((f (#) f) || A) + ((f (#) g) || A)) | (A /\ A) is bounded & (((f (#) g) || A) + ((g (#) g) || A)) | (A /\ A) is bounded ) by RFUNCT_1:100;
assume ( f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A ) ; :: thesis: |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)|||
then A4: ( (f (#) f) || A is integrable & (f (#) g) || A is integrable & (g (#) g) || A is integrable ) by INTEGRA5:def 2;
then A5: ( ((f (#) f) || A) + ((f (#) g) || A) is integrable & ((f (#) g) || A) + ((g (#) g) || A) is integrable ) by A1, A2, INTEGRA1:59;
|||((f + g),(f + g),A)||| = integral (((f (#) (f + g)) + (g (#) (f + g))) || A) by RFUNCT_1:22
.= integral (((f (#) (f + g)) || A) + ((g (#) (f + g)) || A)) by INTEGRA5:5
.= integral ((((f (#) f) + (f (#) g)) || A) + ((g (#) (f + g)) || A)) by RFUNCT_1:23
.= integral ((((f (#) f) + (f (#) g)) || A) + (((g (#) f) + (g (#) g)) || A)) by RFUNCT_1:23
.= integral ((((f (#) f) || A) + ((f (#) g) || A)) + (((g (#) f) + (g (#) g)) || A)) by INTEGRA5:5
.= integral ((((f (#) f) || A) + ((f (#) g) || A)) + (((g (#) f) || A) + ((g (#) g) || A))) by INTEGRA5:5
.= (integral (((f (#) f) || A) + ((f (#) g) || A))) + (integral (((f (#) g) || A) + ((g (#) g) || A))) by A1, A3, A5, INTEGRA1:59
.= ((integral ((f (#) f) || A)) + (integral ((f (#) g) || A))) + (integral (((f (#) g) || A) + ((g (#) g) || A))) by A1, A2, A4, INTEGRA1:59
.= ((integral ((f (#) f) || A)) + (integral ((f (#) g) || A))) + ((integral ((f (#) g) || A)) + (integral ((g (#) g) || A))) by A1, A2, A4, INTEGRA1:59 ;
hence |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| ; :: thesis: verum