let n be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n)

for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f & f is_integrable_on A holds

( g is_integrable_on A & integral (f,A) = integral (g,A) )

let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,(REAL n)

for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f & f is_integrable_on A holds

( g is_integrable_on A & integral (f,A) = integral (g,A) )

let f be PartFunc of REAL,(REAL n); :: thesis: for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f & f is_integrable_on A holds

( g is_integrable_on A & integral (f,A) = integral (g,A) )

let g be PartFunc of REAL,(REAL-NS n); :: thesis: ( f = g & f | A is bounded & A c= dom f & f is_integrable_on A implies ( g is_integrable_on A & integral (f,A) = integral (g,A) ) )

assume A1: ( f = g & f | A is bounded & A c= dom f & f is_integrable_on A ) ; :: thesis: ( g is_integrable_on A & integral (f,A) = integral (g,A) )

hence g is_integrable_on A by Th43; :: thesis: integral (f,A) = integral (g,A)

reconsider h = f | A as Function of A,(REAL n) by Lm3, A1;

reconsider k = h as Function of A,(REAL-NS n) by REAL_NS1:def 4;

A2: integral (f,A) = integral h by INTEGR15:14;

A3: h is bounded by A1;

h is integrable by A1, INTEGR15:13;

then integral h = integral k by A3, Th42;

hence integral (f,A) = integral (g,A) by A2, A1, INTEGR18:9; :: thesis: verum

for f being PartFunc of REAL,(REAL n)

for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f & f is_integrable_on A holds

( g is_integrable_on A & integral (f,A) = integral (g,A) )

let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,(REAL n)

for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f & f is_integrable_on A holds

( g is_integrable_on A & integral (f,A) = integral (g,A) )

let f be PartFunc of REAL,(REAL n); :: thesis: for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f & f is_integrable_on A holds

( g is_integrable_on A & integral (f,A) = integral (g,A) )

let g be PartFunc of REAL,(REAL-NS n); :: thesis: ( f = g & f | A is bounded & A c= dom f & f is_integrable_on A implies ( g is_integrable_on A & integral (f,A) = integral (g,A) ) )

assume A1: ( f = g & f | A is bounded & A c= dom f & f is_integrable_on A ) ; :: thesis: ( g is_integrable_on A & integral (f,A) = integral (g,A) )

hence g is_integrable_on A by Th43; :: thesis: integral (f,A) = integral (g,A)

reconsider h = f | A as Function of A,(REAL n) by Lm3, A1;

reconsider k = h as Function of A,(REAL-NS n) by REAL_NS1:def 4;

A2: integral (f,A) = integral h by INTEGR15:14;

A3: h is bounded by A1;

h is integrable by A1, INTEGR15:13;

then integral h = integral k by A3, Th42;

hence integral (f,A) = integral (g,A) by A2, A1, INTEGR18:9; :: thesis: verum