let X be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of X
for A being 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 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 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 AS: ( 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:3;
then f is Function of (dom f), the carrier of X by FUNCT_2:4;
then reconsider g = f | A as Function of A, the carrier of X by AS, FUNCT_2:38;
P1: 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 )
P11: for i being Element of NAT holds middle_sum (g,(S . i)) = 0. X

proof

let i be Element of NAT ; :: thesis: middle_sum (g,(S . i)) = 0. X
A1: len (S . i) = len (S . i) ;

now

let k be Element of 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 P214: ( 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 Def5;
then A11: k in dom (T . i) by FINSEQ_1:def 3;
then consider c being VECTOR of X such that
A12: ( c in rng (g | (divset ((T . i),k))) & (S . i) . k = (vol (divset ((T . i),k))) * c ) by Def5;
( 0 <= vol (divset ((T . i),k)) & vol (divset ((T . i),k)) <= 0 ) by AS, INTEGRA1:11, INTEGRA2:40, A11, INTEGRA1:10;
then A13: vol (divset ((T . i),k)) = 0 ;
(S . i) . k = 0. X by A13, A12, RLVECT_1:23;
hence (S . i) . k = - v by RLVECT_1:25, P214; :: thesis: verum

end;

then Sum (S . i) = - (Sum (S . i)) by A1, RLVECT_1:57;
hence middle_sum (g,(S . i)) = 0. X by RLVECT_1:33; :: thesis: verum

end;

P12: for i being Element of NAT holds (middle_sum (g,S)) . i = 0. X

proof

let i be Element of NAT ; :: thesis: (middle_sum (g,S)) . i = 0. X
thus (middle_sum (g,S)) . i = middle_sum (g,(S . i)) by Def8
.= 0. X by P11 ; :: thesis: verum

end;

P13: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of 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 Element of NAT st
for n being Element of NAT st m <= n holds
||.(((middle_sum (g,S)) . n) - (0. X)).|| < r )
assume AS: 0 < r ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((middle_sum (g,S)) . n) - (0. X)).|| < r
take m = 0 ; :: thesis: for n being Element of NAT st m <= n holds
||.(((middle_sum (g,S)) . n) - (0. X)).|| < r
let n be Element of 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 P12
.= 0 by NORMSP_1:10 ;
hence ||.(((middle_sum (g,S)) . n) - (0. X)).|| < r by AS; :: thesis: verum

end;

hence middle_sum (g,S) is convergent by NORMSP_1:def 9; :: thesis: lim (middle_sum (g,S)) = 0. X
hence lim (middle_sum (g,S)) = 0. X by P13, NORMSP_1:def 11; :: thesis: verum

end;

then P2: g is integrable by Def13;
hence f is_integrable_on A by Def16; :: thesis: integral (f,A) = 0. X
integral g = 0. X by P2, P1, Def14;
hence integral (f,A) = 0. X by Def17, AS; :: thesis: verum