let f, g be PartFunc of REAL,REAL; 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; ( (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 )
; ( 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
; |||((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; verum