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 holds
( f is_integrable_on A iff g is_integrable_on 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 holds
( f is_integrable_on A iff g is_integrable_on 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 holds
( f is_integrable_on A iff g is_integrable_on A )
let g be PartFunc of REAL,(REAL-NS n); :: thesis: ( f = g & f | A is bounded & A c= dom f implies ( f is_integrable_on A iff g is_integrable_on A ) )
assume A1: ( f = g & f | A is bounded & A c= dom f ) ; :: thesis: ( f is_integrable_on A iff g is_integrable_on 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: h is bounded by A1;

hereby :: thesis: ( g is_integrable_on A implies f is_integrable_on A )

assume f is_integrable_on A ; :: thesis: g is_integrable_on A
then h is integrable by INTEGR15:13;
then k is integrable by A2, Th41;
hence g is_integrable_on A by A1; :: thesis: verum

end;

assume g is_integrable_on A ; :: thesis: f is_integrable_on A
then k is integrable by A1;
then h is integrable by A2, Th41;
hence f is_integrable_on A by INTEGR15:13; :: thesis: verum