let f, g be PartFunc of REAL,REAL; :: thesis: for A being non empty 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 non empty 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 that
A1: (f (#) f) || A is total and
A2: (f (#) g) || A is total and
A3: (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 that
A4: ((f (#) f) || A) | A is bounded and
A5: ((f (#) g) || A) | A is bounded and
A6: ((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)||| )
assume that
A7: f (#) f is_integrable_on A and
A8: f (#) g is_integrable_on A and
A9: g (#) g is_integrable_on A ; :: thesis: |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)|||
A10: (f (#) g) || A is integrable by A8;
A11: (g (#) g) || A is integrable by A9;
then A12: ((f (#) g) || A) + ((g (#) g) || A) is integrable by A2, A3, A5, A6, A10, INTEGRA1:57;
A13: (f (#) f) || A is integrable by A7;
then A14: ((f (#) f) || A) + ((f (#) g) || A) is integrable by A1, A2, A4, A5, A10, INTEGRA1:57;
A15: ( (((f (#) f) || A) + ((f (#) g) || A)) | (A /\ A) is bounded & (((f (#) g) || A) + ((g (#) g) || A)) | (A /\ A) is bounded ) by A4, A5, A6, RFUNCT_1:83;
|||((f + g),(f + g),A)||| = integral (((f (#) (f + g)) + (g (#) (f + g))) || A) by RFUNCT_1:10
.= 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:11
.= integral ((((f (#) f) + (f (#) g)) || A) + (((g (#) f) + (g (#) g)) || A)) by RFUNCT_1:11
.= 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, A2, A3, A15, A14, A12, INTEGRA1:57
.= ((integral ((f (#) f) || A)) + (integral ((f (#) g) || A))) + (integral (((f (#) g) || A) + ((g (#) g) || A))) by A1, A2, A4, A5, A13, A10, INTEGRA1:57
.= ((integral ((f (#) f) || A)) + (integral ((f (#) g) || A))) + ((integral ((f (#) g) || A)) + (integral ((g (#) g) || A))) by A2, A3, A5, A6, A10, A11, INTEGRA1:57 ;
hence |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| ; :: thesis: verum