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 & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) & ( for x being Real st x in A holds
((g (#) g) || A) . x >= 0 ) holds
||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2)
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 & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) & ( for x being Real st x in A holds
((g (#) g) || A) . x >= 0 ) implies ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) )
assume that
A1: (f (#) f) || A is total and
A2: (f (#) g) || A is total and
A3: (g (#) g) || A is total and
A4: ((f (#) f) || A) | A is bounded and
A5: ((f (#) g) || A) | A is bounded and
A6: ((g (#) g) || A) | A is bounded and
A7: ( 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 ex x being Real st
( x in A & not ((f (#) f) || A) . x >= 0 ) or ex x being Real st
( x in A & not ((g (#) g) || A) . x >= 0 ) or ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) )
assume A8: f is_orthogonal_with g,A ; :: thesis: ( ex x being Real st
( x in A & not ((f (#) f) || A) . x >= 0 ) or ex x being Real st
( x in A & not ((g (#) g) || A) . x >= 0 ) or ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) )
assume for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ; :: thesis: ( ex x being Real st
( x in A & not ((g (#) g) || A) . x >= 0 ) or ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) )
then A9: |||(f,f,A)||| >= 0 by A1, A4, INTEGRA2:32;
assume for x being Real st x in A holds
((g (#) g) || A) . x >= 0 ; :: thesis: ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2)
then A10: |||(g,g,A)||| >= 0 by A3, A6, INTEGRA2:32;
then A11: ||..g,A..|| ^2 = |||(g,g,A)||| by SQUARE_1:def 2;
|||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)||| by A1, A2, A3, A4, A5, A6, A7, A8, Th32;
then |||((f + g),(f + g),A)||| >= 0 by A9, A10, XREAL_1:33;
then A12: ||..(f + g),A..|| ^2 = |||((f + g),(f + g),A)||| by SQUARE_1:def 2;
||..f,A..|| ^2 = |||(f,f,A)||| by A9, SQUARE_1:def 2;
hence ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) by A1, A2, A3, A4, A5, A6, A7, A8, A12, A11, Th32; :: thesis: verum