let f be PartFunc of REAL,REAL; :: thesis: for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) holds
0 <= ||..f,A..||
let A be non empty closed_interval Subset of REAL; :: thesis: ( (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & ( 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 ex x being Real st
( x in A & not ((f (#) f) || A) . x >= 0 ) or 0 <= ||..f,A..|| )
assume ( ((f (#) f) || A) | A is bounded & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) ) ; :: thesis: 0 <= ||..f,A..||
then |||(f,f,A)||| >= 0 by A1, INTEGRA2:32;
hence 0 <= ||..f,A..|| by SQUARE_1:def 2; :: thesis: verum