let n be Element of NAT ; 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; 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); 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); ( 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 )
; ( g is_integrable_on A & integral (f,A) = integral (g,A) )
hence
g is_integrable_on A
by Th43; 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; verum