let n be Element of NAT ; :: thesis: for a, b, c, d being Real
for f being PartFunc of REAL,()
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,()
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,(); :: 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 ;
then A2: ( a <= c & d <= b & a <= d & c <= b ) by ;
A3: g | ['a,b'] is bounded by ;
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
.= integral (f,c,d) by A6, A7, A1, Th47 ; :: thesis: verum
end;
end;