theorem :: INTEGRA9:45

for f, g being 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 & ( 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)