let X be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of X

for A being non empty closed_interval Subset of REAL st vol A = 0 & A c= dom f holds

( f is_integrable_on A & integral (f,A) = 0. X )

let f be PartFunc of REAL, the carrier of X; :: thesis: for A being non empty closed_interval Subset of REAL st vol A = 0 & A c= dom f holds

( f is_integrable_on A & integral (f,A) = 0. X )

let A be non empty closed_interval Subset of REAL; :: thesis: ( vol A = 0 & A c= dom f implies ( f is_integrable_on A & integral (f,A) = 0. X ) )

assume A1: ( vol A = 0 & A c= dom f ) ; :: thesis: ( f is_integrable_on A & integral (f,A) = 0. X )

f is Function of (dom f),(rng f) by FUNCT_2:1;

then f is Function of (dom f), the carrier of X by FUNCT_2:2;

then reconsider g = f | A as Function of A, the carrier of X by A1, FUNCT_2:32;

A2: 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)) = 0. X )

hence f is_integrable_on A ; :: thesis: integral (f,A) = 0. X

integral g = 0. X by A12, A2, Def6;

hence integral (f,A) = 0. X by Def8, A1; :: thesis: verum

for A being non empty closed_interval Subset of REAL st vol A = 0 & A c= dom f holds

( f is_integrable_on A & integral (f,A) = 0. X )

let f be PartFunc of REAL, the carrier of X; :: thesis: for A being non empty closed_interval Subset of REAL st vol A = 0 & A c= dom f holds

( f is_integrable_on A & integral (f,A) = 0. X )

let A be non empty closed_interval Subset of REAL; :: thesis: ( vol A = 0 & A c= dom f implies ( f is_integrable_on A & integral (f,A) = 0. X ) )

assume A1: ( vol A = 0 & A c= dom f ) ; :: thesis: ( f is_integrable_on A & integral (f,A) = 0. X )

f is Function of (dom f),(rng f) by FUNCT_2:1;

then f is Function of (dom f), the carrier of X by FUNCT_2:2;

then reconsider g = f | A as Function of A, the carrier of X by A1, FUNCT_2:32;

A2: 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)) = 0. X )

proof

then A12:
g is integrable
;
let T be DivSequence of A; :: thesis: 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)) = 0. X )

let S be middle_volume_Sequence of g,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = 0. X ) )

assume ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = 0. X )

A3: for i being Nat holds middle_sum (g,(S . i)) = 0. X

ex m being Nat st

for n being Nat st m <= n holds

||.(((middle_sum (g,S)) . n) - (0. X)).|| < r

hence lim (middle_sum (g,S)) = 0. X by A10, NORMSP_1:def 7; :: thesis: verum

end;( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = 0. X )

let S be middle_volume_Sequence of g,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = 0. X ) )

assume ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = 0. X )

A3: for i being Nat holds middle_sum (g,(S . i)) = 0. X

proof

A9:
for i being Nat holds (middle_sum (g,S)) . i = 0. X
let i be Nat; :: thesis: middle_sum (g,(S . i)) = 0. X

A4: len (S . i) = len (S . i) ;

hence middle_sum (g,(S . i)) = 0. X by RLVECT_1:19; :: thesis: verum

end;A4: len (S . i) = len (S . i) ;

now :: thesis: for k being Nat

for v being Element of X st k in dom (S . i) & v = (S . i) . k holds

(S . i) . k = - v

then
Sum (S . i) = - (Sum (S . i))
by A4, RLVECT_1:40;for v being Element of X st k in dom (S . i) & v = (S . i) . k holds

(S . i) . k = - v

let k be Nat; :: thesis: for v being Element of X st k in dom (S . i) & v = (S . i) . k holds

(S . i) . k = - v

let v be Element of X; :: thesis: ( k in dom (S . i) & v = (S . i) . k implies (S . i) . k = - v )

assume A5: ( k in dom (S . i) & v = (S . i) . k ) ; :: thesis: (S . i) . k = - v

then k in Seg (len (S . i)) by FINSEQ_1:def 3;

then k in Seg (len (T . i)) by Def1;

then A6: k in dom (T . i) by FINSEQ_1:def 3;

then consider c being VECTOR of X such that

A7: ( c in rng (g | (divset ((T . i),k))) & (S . i) . k = (vol (divset ((T . i),k))) * c ) by Def1;

( 0 <= vol (divset ((T . i),k)) & vol (divset ((T . i),k)) <= 0 ) by A1, A6, INTEGRA1:8, INTEGRA1:9, INTEGRA2:38;

then A8: vol (divset ((T . i),k)) = 0 ;

(S . i) . k = 0. X by A8, A7, RLVECT_1:10;

hence (S . i) . k = - v by A5, RLVECT_1:12; :: thesis: verum

end;(S . i) . k = - v

let v be Element of X; :: thesis: ( k in dom (S . i) & v = (S . i) . k implies (S . i) . k = - v )

assume A5: ( k in dom (S . i) & v = (S . i) . k ) ; :: thesis: (S . i) . k = - v

then k in Seg (len (S . i)) by FINSEQ_1:def 3;

then k in Seg (len (T . i)) by Def1;

then A6: k in dom (T . i) by FINSEQ_1:def 3;

then consider c being VECTOR of X such that

A7: ( c in rng (g | (divset ((T . i),k))) & (S . i) . k = (vol (divset ((T . i),k))) * c ) by Def1;

( 0 <= vol (divset ((T . i),k)) & vol (divset ((T . i),k)) <= 0 ) by A1, A6, INTEGRA1:8, INTEGRA1:9, INTEGRA2:38;

then A8: vol (divset ((T . i),k)) = 0 ;

(S . i) . k = 0. X by A8, A7, RLVECT_1:10;

hence (S . i) . k = - v by A5, RLVECT_1:12; :: thesis: verum

hence middle_sum (g,(S . i)) = 0. X by RLVECT_1:19; :: thesis: verum

proof

A10:
for r being Real st 0 < r holds
let i be Nat; :: thesis: (middle_sum (g,S)) . i = 0. X

thus (middle_sum (g,S)) . i = middle_sum (g,(S . i)) by Def4

.= 0. X by A3 ; :: thesis: verum

end;thus (middle_sum (g,S)) . i = middle_sum (g,(S . i)) by Def4

.= 0. X by A3 ; :: thesis: verum

ex m being Nat st

for n being Nat st m <= n holds

||.(((middle_sum (g,S)) . n) - (0. X)).|| < r

proof

hence
middle_sum (g,S) is convergent
by NORMSP_1:def 6; :: thesis: lim (middle_sum (g,S)) = 0. X
let r be Real; :: thesis: ( 0 < r implies ex m being Nat st

for n being Nat st m <= n holds

||.(((middle_sum (g,S)) . n) - (0. X)).|| < r )

assume A11: 0 < r ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

||.(((middle_sum (g,S)) . n) - (0. X)).|| < r

take m = 0 ; :: thesis: for n being Nat st m <= n holds

||.(((middle_sum (g,S)) . n) - (0. X)).|| < r

let n be Nat; :: thesis: ( m <= n implies ||.(((middle_sum (g,S)) . n) - (0. X)).|| < r )

assume m <= n ; :: thesis: ||.(((middle_sum (g,S)) . n) - (0. X)).|| < r

||.(((middle_sum (g,S)) . n) - (0. X)).|| = ||.((0. X) - (0. X)).|| by A9

.= 0 by NORMSP_1:6 ;

hence ||.(((middle_sum (g,S)) . n) - (0. X)).|| < r by A11; :: thesis: verum

end;for n being Nat st m <= n holds

||.(((middle_sum (g,S)) . n) - (0. X)).|| < r )

assume A11: 0 < r ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

||.(((middle_sum (g,S)) . n) - (0. X)).|| < r

take m = 0 ; :: thesis: for n being Nat st m <= n holds

||.(((middle_sum (g,S)) . n) - (0. X)).|| < r

let n be Nat; :: thesis: ( m <= n implies ||.(((middle_sum (g,S)) . n) - (0. X)).|| < r )

assume m <= n ; :: thesis: ||.(((middle_sum (g,S)) . n) - (0. X)).|| < r

||.(((middle_sum (g,S)) . n) - (0. X)).|| = ||.((0. X) - (0. X)).|| by A9

.= 0 by NORMSP_1:6 ;

hence ||.(((middle_sum (g,S)) . n) - (0. X)).|| < r by A11; :: thesis: verum

hence lim (middle_sum (g,S)) = 0. X by A10, NORMSP_1:def 7; :: thesis: verum

hence f is_integrable_on A ; :: thesis: integral (f,A) = 0. X

integral g = 0. X by A12, A2, Def6;

hence integral (f,A) = 0. X by Def8, A1; :: thesis: verum