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 )

proof

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

proof

let i be Nat; :: thesis: middle_sum (g,(S . i)) = 0. X
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

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;

then Sum (S . i) = - (Sum (S . i)) by A4, RLVECT_1:40;
hence middle_sum (g,(S . i)) = 0. X by RLVECT_1:19; :: thesis: verum

end;

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

proof

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;

A10: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.(((middle_sum (g,S)) . n) - (0. X)).|| < r

proof

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;

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

end;

then A12: g is integrable ;
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