let n be Element of NAT ; :: thesis: for a, b, c, d being Real
for f being PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL n) st f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = integral (g,c,d)
let a, b, c, d be Real; :: thesis: for f being PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL n) st f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = integral (g,c,d)
let f be PartFunc of REAL,(REAL-NS n); :: thesis: for g being PartFunc of REAL,(REAL n) st f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = integral (g,c,d)
let g be PartFunc of REAL,(REAL n); :: thesis: ( f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] implies integral (f,c,d) = integral (g,c,d) )
assume A1: ( f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: integral (f,c,d) = integral (g,c,d)
['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then A2: ( a <= c & d <= b & a <= d & c <= b ) by A1, XXREAL_1:1;
A3: g | ['a,b'] is bounded by A1, Th34;
A4: g is_integrable_on ['a,b'] by Th43, A3, A1;

per cases ( c <= d or not c <= d ) ;

suppose A5: c <= d ; :: thesis: integral (f,c,d) = integral (g,c,d)

( ['c,d'] c= dom g & g | ['c,d'] is bounded & g is_integrable_on ['c,d'] ) by A3, A4, A1, Th9, A2, A5, Th2;
hence integral (f,c,d) = integral (g,c,d) by A1, A5, Th45; :: thesis: verum

end;

suppose A6: not c <= d ; :: thesis: integral (f,c,d) = integral (g,c,d)

A7: ( ['d,c'] c= dom g & g | ['d,c'] is bounded & g is_integrable_on ['d,c'] ) by A3, A4, A1, Th9, A2, A6, Th2;
then A8: integral (f,d,c) = integral (g,d,c) by A1, A6, Th45;
thus integral (g,c,d) = - (integral (g,d,c)) by Th33
.= - (integral (f,d,c)) by A8, REAL_NS1:4
.= integral (f,c,d) by A6, A7, A1, Th47 ; :: thesis: verum

end;

end;