let n be non zero Element of NAT ; 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; 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); ( 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'] )
; ( ||.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; verum