let a, b, c, d be Real; :: thesis: for f being PartFunc of REAL,REAL st 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

( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) )

let f be PartFunc of REAL,REAL; :: thesis: ( 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 ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) ) )

assume A1: ( 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: ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) )

( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) )

let f be PartFunc of REAL,REAL; :: thesis: ( 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 ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) ) )

assume A1: ( 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: ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) )

A2: now :: thesis: ( not c <= d implies ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) ) )

assume A3:
not c <= d
; :: thesis: ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) )

then integral (f,c,d) = - (integral (f,['d,c'])) by INTEGRA5:def 4;

then integral (f,c,d) = - (integral (f,d,c)) by A3, INTEGRA5:def 4;

then A4: |.(integral (f,c,d)).| = |.(integral (f,d,c)).| by COMPLEX1:52;

( d = min (c,d) & c = max (c,d) ) by A3, XXREAL_0:def 9, XXREAL_0:def 10;

hence ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) ) by A1, A3, A4, Lm5; :: thesis: verum

end;then integral (f,c,d) = - (integral (f,['d,c'])) by INTEGRA5:def 4;

then integral (f,c,d) = - (integral (f,d,c)) by A3, INTEGRA5:def 4;

then A4: |.(integral (f,c,d)).| = |.(integral (f,d,c)).| by COMPLEX1:52;

( d = min (c,d) & c = max (c,d) ) by A3, XXREAL_0:def 9, XXREAL_0:def 10;

hence ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) ) by A1, A3, A4, Lm5; :: thesis: verum

now :: thesis: ( c <= d implies ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) ) )

hence
( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) )
by A2; :: thesis: verumassume A5:
c <= d
; :: thesis: ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) )

then ( c = min (c,d) & d = max (c,d) ) by XXREAL_0:def 9, XXREAL_0:def 10;

hence ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) ) by A1, A5, Lm5; :: thesis: verum

end;then ( c = min (c,d) & d = max (c,d) ) by XXREAL_0:def 9, XXREAL_0:def 10;

hence ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) ) by A1, A5, Lm5; :: thesis: verum