let f be PartFunc of REAL ,REAL ; :: thesis: for A being closed-interval Subset of REAL st (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & (f (#) f) || A is integrable & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) holds
0 <= ||..f,A..||
let A be closed-interval Subset of REAL ; :: thesis: ( (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & (f (#) f) || A is integrable & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) implies 0 <= ||..f,A..|| )
assume A1: (f (#) f) || A is total ; :: thesis: ( not ((f (#) f) || A) | A is bounded or not (f (#) f) || A is integrable or ex x being Real st
( x in A & not ((f (#) f) || A) . x >= 0 ) or 0 <= ||..f,A..|| )
assume A2: ( ((f (#) f) || A) | A is bounded & (f (#) f) || A is integrable & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) ) ; :: thesis: 0 <= ||..f,A..||
|||(f,f,A)||| >= 0 by A1, A2, INTEGRA2:32;
hence 0 <= ||..f,A..|| by SQUARE_1:def 4; :: thesis: verum