let n be Element of NAT ; :: thesis: for a, b being Real
for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n) st f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] holds
integral (f,a,b) = integral (g,a,b)
let a, b be Real; :: thesis: for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n) st f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] holds
integral (f,a,b) = integral (g,a,b)
let f be PartFunc of REAL,(REAL n); :: thesis: for g being PartFunc of REAL,(REAL-NS n) st f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] holds
integral (f,a,b) = integral (g,a,b)
let g be PartFunc of REAL,(REAL-NS n); :: thesis: ( f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] implies integral (f,a,b) = integral (g,a,b) )
assume A1: ( f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] ) ; :: thesis: integral (f,a,b) = integral (g,a,b)
A2: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
A3: integral (g,['a,b']) = integral (f,['a,b']) by A1, Th44;
integral (g,['a,b']) = integral (g,a,b) by A2, INTEGR18:16;
hence integral (f,a,b) = integral (g,a,b) by A3, A2, INTEGR15:19; :: thesis: verum