let n be Element of NAT ; :: thesis: 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 holds

( f is integrable iff g is integrable )

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

for g being Function of A,(REAL-NS n) st f = g & f is bounded holds

( f is integrable iff g is integrable )

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

( f is integrable iff g is integrable )

let g be Function of A,(REAL-NS n); :: thesis: ( f = g & f is bounded implies ( f is integrable iff g is integrable ) )

assume A1: ( f = g & f is bounded ) ; :: thesis: ( f is integrable iff g is integrable )

then consider I being Point of (REAL-NS n) such that

A3: for T being DivSequence of A

for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = I ) ;

reconsider I0 = I as Element of REAL n by REAL_NS1:def 4;

I0 = I ;

then for T being DivSequence of A

for S0 being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I0 ) by A3, A1, Th40;

hence f is integrable by A1, INTEGR15:12; :: thesis: verum

for f being Function of A,(REAL n)

for g being Function of A,(REAL-NS n) st f = g & f is bounded holds

( f is integrable iff g is integrable )

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

for g being Function of A,(REAL-NS n) st f = g & f is bounded holds

( f is integrable iff g is integrable )

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

( f is integrable iff g is integrable )

let g be Function of A,(REAL-NS n); :: thesis: ( f = g & f is bounded implies ( f is integrable iff g is integrable ) )

assume A1: ( f = g & f is bounded ) ; :: thesis: ( f is integrable iff g is integrable )

hereby :: thesis: ( g is integrable implies f is integrable )

assume
g is integrable
; :: thesis: f is integrable assume
f is integrable
; :: thesis: g is integrable

then consider I being Element of REAL n such that

A2: 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)) = I ) by A1, INTEGR15:12;

reconsider I0 = I as Point of (REAL-NS n) by REAL_NS1:def 4;

I = 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 A2, A1, Th40;

hence g is integrable ; :: thesis: verum

end;then consider I being Element of REAL n such that

A2: 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)) = I ) by A1, INTEGR15:12;

reconsider I0 = I as Point of (REAL-NS n) by REAL_NS1:def 4;

I = 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 A2, A1, Th40;

hence g is integrable ; :: thesis: verum

then consider I being Point of (REAL-NS n) such that

A3: for T being DivSequence of A

for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = I ) ;

reconsider I0 = I as Element of REAL n by REAL_NS1:def 4;

I0 = I ;

then for T being DivSequence of A

for S0 being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I0 ) by A3, A1, Th40;

hence f is integrable by A1, INTEGR15:12; :: thesis: verum