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 & 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 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 A1: ( (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 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 ) )
then B1: ( (f (#) f) || A is integrable & (f (#) g) || A is integrable & (g (#) g) || A is integrable ) by INTEGRA5:def 2;
assume A2: 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 ) )
A3: |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)||| by A1, A2, Th38;
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 A4: |||(f,f,A)||| >= 0 by A1, B1, 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 A5: |||(g,g,A)||| >= 0 by A1, B1, INTEGRA2:32;
|||((f + g),(f + g),A)||| >= 0 by A3, A4, A5, XREAL_1:35;
then A6: ||..(f + g),A..|| ^2 = |||((f + g),(f + g),A)||| by SQUARE_1:def 4;
A7: ||..f,A..|| ^2 = |||(f,f,A)||| by A4, SQUARE_1:def 4;
||..g,A..|| ^2 = |||(g,g,A)||| by A5, SQUARE_1:def 4;
hence ||..(f + g),A..|| ^2 = (||..f,A..|| ^2 ) + (||..g,A..|| ^2 ) by A1, A2, Th38, A6, A7; :: thesis: verum