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;

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 )
;

end;

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;hence integral (f,c,d) = integral (g,c,d) by A1, A5, Th45; :: thesis: verum

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;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