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 & f is_orthogonal_with g,A holds
|||((f + g),(f + g),A)||| = |||(f,f,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 & f is_orthogonal_with g,A implies |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)||| )
assume ( (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 ) ; :: thesis: ( not f is_orthogonal_with g,A or |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)||| )
then A1: |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| by Th31;
assume f is_orthogonal_with g,A ; :: thesis: |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)|||
then |||(f,g,A)||| = 0 ;
hence |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)||| by A1; :: thesis: verum