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))) )
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;
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))) ) )
assume 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;
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: verum