let n be non zero Element of NAT ; :: thesis: for a, b, c, d being Real
for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & ||.f.|| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] & ||.f.|| | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) )
let a, b, c, d be Real; :: thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & ||.f.|| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] & ||.f.|| | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) )
let f be PartFunc of REAL,(REAL-NS n); :: thesis: ( a <= b & f is_integrable_on ['a,b'] & ||.f.|| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies ( ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] & ||.f.|| | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) ) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & ||.f.|| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: ( ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] & ||.f.|| | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) )
reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def 4;
A2: f1 | ['a,b'] is bounded by A1, INTEGR19:34;
A3: f1 is_integrable_on ['a,b'] by A2, A1, INTEGR19:43;
A4: ||.f.|| = |.f1.| by NFCONT_4:9;
A5: |.f1.| is_integrable_on ['a,b'] by A1, NFCONT_4:9;
( |.f1.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f1.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f1,c,d)).| <= integral (|.f1.|,(min (c,d)),(max (c,d))) ) by A1, A2, A3, A5, INTEGR19:22;
hence ( ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] & ||.f.|| | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) ) by A4, REAL_NS1:1, A1, INTEGR19:48; :: thesis: verum