let n be Element of NAT ; for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n) st f = g & f is bounded & f is integrable holds
( g is integrable & integral f = integral g )
let A be non empty closed_interval Subset of REAL; for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n) st f = g & f is bounded & f is integrable holds
( g is integrable & integral f = integral g )
let f be Function of A,(REAL n); for g being Function of A,(REAL-NS n) st f = g & f is bounded & f is integrable holds
( g is integrable & integral f = integral g )
let g be Function of A,(REAL-NS n); ( f = g & f is bounded & f is integrable implies ( g is integrable & integral f = integral g ) )
assume A1:
( f = g & f is bounded & f is integrable )
; ( g is integrable & integral f = integral g )
then A2:
g is integrable
by Th41;
A3:
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
by A1, INTEGR15:11;
reconsider I0 = integral f as Point of (REAL-NS n) by REAL_NS1:def 4;
integral f = I0
;
then
for T being DivSequence of A
for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = I0 )
by A3, A1, Th40;
hence
( g is integrable & integral f = integral g )
by A2, INTEGR18:def 6; verum