let a, b, c, d be real number ; :: 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 & abs (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 & abs (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 & abs (integral f,c,d) <= integral (abs f),(min c,d),(max c,d) )

A2: now

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 & abs (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 5;
then integral f,c,d = - (integral f,d,c) by A3, INTEGRA5:def 5;
then A4: abs (integral f,c,d) = abs (integral f,d,c) by COMPLEX1:138;
( 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 & abs (integral f,c,d) <= integral (abs f),(min c,d),(max c,d) ) by A1, A3, A4, Lm5; :: thesis: verum

end;

now

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 & abs (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 & abs (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 & abs (integral f,c,d) <= integral (abs f),(min c,d),(max c,d) ) by A2; :: thesis: verum