:: INTEGR18 semantic presentation

begin

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A, the carrier of X;
let D be Division of A;
mode middle_volume of f,D ->  FinSequence of X means :Def1: :: INTEGR18:def 1
( len it = len D & ( for i being Nat st i in dom D holds
ex c being Point of X st
( c in rng (f | (divset (D,i))) & it . i = (vol (divset (D,i))) * c ) ) );
correctness
existence
ex b1 being FinSequence of X st
( len b1 = len D & ( for i being Nat st i in dom D holds
ex c being Point of X st
( c in rng (f | (divset (D,i))) & b1 . i = (vol (divset (D,i))) * c ) ) );
proof
defpred S1[ Nat, set ] means  ex c being Point of X st
( c in rng (f | (divset (D,$1))) & $2 = (vol (divset (D,$1))) * c );
A1: Seg (len D) = dom D by FINSEQ_1:def_3;
A2: for k being Nat st k in Seg (len D) holds
ex x being Element of the carrier of X st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len D) implies ex x being Element of the carrier of X st S1[k,x] )
assume  k in Seg (len D) ; ::_thesis: ex x being Element of the carrier of X st S1[k,x]
then A3: k in dom D by FINSEQ_1:def_3;
 dom f = A by FUNCT_2:def_1;
then  dom (f | (divset (D,k))) = divset (D,k) by A3, INTEGRA1:8, RELAT_1:62;
then  not rng (f | (divset (D,k))) is empty by RELAT_1:42;
then consider c being set  such that
A4: c in rng (f | (divset (D,k))) by XBOOLE_0:def_1;
reconsider c = c as Point of X by A4;
 (vol (divset (D,k))) * c is Element of the carrier of X ;
hence  ex x being Element of the carrier of X st S1[k,x] by A4; ::_thesis: verum
end;
consider p being FinSequence of the carrier of X such that
A5: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds
S1[k,p . k] ) ) from FINSEQ_1:sch_5(A2);
 len p = len D by A5, FINSEQ_1:def_3;
hence  ex b1 being FinSequence of X st
( len b1 = len D & ( for i being Nat st i in dom D holds
ex c being Point of X st
( c in rng (f | (divset (D,i))) & b1 . i = (vol (divset (D,i))) * c ) ) ) by A5, A1; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines middle_volume INTEGR18:def_1_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X
for D being Division of A
for b5 being FinSequence of X holds
( b5 is middle_volume of f,D iff ( len b5 = len D & ( for i being Nat st i in dom D holds
ex c being Point of X st
( c in rng (f | (divset (D,i))) & b5 . i = (vol (divset (D,i))) * c ) ) ) );

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A, the carrier of X;
let D be Division of A;
let F be middle_volume of f,D;
func middle_sum (f,F) ->  Point of X equals :: INTEGR18:def 2
 Sum F;
coherence
 Sum F is Point of X ;
end;

:: deftheorem  defines middle_sum INTEGR18:def_2_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X
for D being Division of A
for F being middle_volume of f,D holds middle_sum (f,F) = Sum F;

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A, the carrier of X;
let T be DivSequence of A;
mode middle_volume_Sequence of f,T ->  Function of NAT,( the carrier of X *) means :Def3: :: INTEGR18:def 3
 for k being Element of NAT holds it . k is middle_volume of f,T . k;
correctness
existence
ex b1 being Function of NAT,( the carrier of X *) st
for k being Element of NAT holds b1 . k is middle_volume of f,T . k;
proof
defpred S1[ Element of NAT , set ] means $2 is middle_volume of f,T . $1;
A1: for x being Element of NAT ex y being Element of the carrier of X * st S1[x,y]
proof
let x be Element of NAT ; ::_thesis: ex y being Element of the carrier of X * st S1[x,y]
set y = the middle_volume of f,T . x;
reconsider y = the middle_volume of f,T . x as Element of the carrier of X * by FINSEQ_1:def_11;
 y is middle_volume of f,T . x ;
hence  ex y being Element of the carrier of X * st S1[x,y] ; ::_thesis: verum
end;
 ex f being Function of NAT,( the carrier of X *) st
for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A1);
hence  ex b1 being Function of NAT,( the carrier of X *) st
for k being Element of NAT holds b1 . k is middle_volume of f,T . k ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines middle_volume_Sequence INTEGR18:def_3_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X
for T being DivSequence of A
for b5 being Function of NAT,( the carrier of X *) holds
( b5 is middle_volume_Sequence of f,T iff for k being Element of NAT holds b5 . k is middle_volume of f,T . k );

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A, the carrier of X;
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
let k be Element of NAT ;
:: original: .
redefine funcS . k ->  middle_volume of f,T . k;
coherence
 S . k is middle_volume of f,T . k by Def3;
end;

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A, the carrier of X;
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
func middle_sum (f,S) ->  sequence of X means :Def4: :: INTEGR18:def 4
 for i being Element of NAT holds it . i = middle_sum (f,(S . i));
existence
 ex b1 being sequence of X st
for i being Element of NAT holds b1 . i = middle_sum (f,(S . i))
proof
deffunc H1( Element of NAT ) ->  Point of X = middle_sum (f,(S . $1));
thus  ex IT being sequence of the carrier of X st
for i being Element of NAT holds IT . i = H1(i) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being sequence of X st ( for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds b2 . i = middle_sum (f,(S . i)) ) holds
b1 = b2
proof
let F1, F2 be sequence of X; ::_thesis: ( ( for i being Element of NAT holds F1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds F2 . i = middle_sum (f,(S . i)) ) implies F1 = F2 )
assume that
A1: for i being Element of NAT holds F1 . i = middle_sum (f,(S . i)) and
A2: for i being Element of NAT holds F2 . i = middle_sum (f,(S . i)) ; ::_thesis: F1 = F2
 for i being Element of NAT holds F1 . i = F2 . i
proof
let i be Element of NAT ; ::_thesis: F1 . i = F2 . i
F1 . i = middle_sum (f,(S . i)) by A1
.= F2 . i by A2 ;
hence  F1 . i = F2 . i ; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines middle_sum INTEGR18:def_4_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for b6 being sequence of X holds
( b6 = middle_sum (f,S) iff for i being Element of NAT holds b6 . i = middle_sum (f,(S . i)) );

begin

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A, the carrier of X;
attrf is integrable  means :Def5: :: INTEGR18:def 5
 ex I being Point of X st
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 );
end;

:: deftheorem Def5 defines integrable INTEGR18:def_5_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X holds
( f is integrable iff ex I being Point of X st
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 ) );

theorem Th1: :: INTEGR18:1
for X being RealNormSpace
for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 + R2 holds
Sum R3 = (Sum R1) + (Sum R2)
proof
let X be RealNormSpace; ::_thesis: for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 + R2 holds
Sum R3 = (Sum R1) + (Sum R2)
let R1, R2, R3 be FinSequence of X; ::_thesis: ( len R1 = len R2 & R3 = R1 + R2 implies Sum R3 = (Sum R1) + (Sum R2) )
assume A1: ( len R1 = len R2 & R3 = R1 + R2 ) ; ::_thesis: Sum R3 = (Sum R1) + (Sum R2)
then  dom R1 = dom R2 by FINSEQ_3:29;
hence  Sum R3 = (Sum R1) + (Sum R2) by A1, BINOM:7; ::_thesis: verum
end;

theorem :: INTEGR18:2
for X being RealNormSpace
for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 - R2 holds
Sum R3 = (Sum R1) - (Sum R2)
proof
let X be RealNormSpace; ::_thesis: for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 - R2 holds
Sum R3 = (Sum R1) - (Sum R2)
let R1, R2, R3 be FinSequence of X; ::_thesis: ( len R1 = len R2 & R3 = R1 - R2 implies Sum R3 = (Sum R1) - (Sum R2) )
assume A1: ( len R1 = len R2 & R3 = R1 - R2 ) ; ::_thesis: Sum R3 = (Sum R1) - (Sum R2)
then A2: dom R1 = dom R2 by FINSEQ_3:29;
A3: dom R3 = (dom R1) /\ (dom R2) by A1, VFUNCT_1:def_2
.= dom R1 by A2 ;
then A4: len R3 = len R1 by FINSEQ_3:29;
A5: for k being Element of NAT st k in dom R1 holds
R3 . k = (R1 /. k) - (R2 /. k)
proof
let k be Element of NAT ; ::_thesis: ( k in dom R1 implies R3 . k = (R1 /. k) - (R2 /. k) )
assume A6: k in dom R1 ; ::_thesis: R3 . k = (R1 /. k) - (R2 /. k)
thus R3 . k = R3 /. k by A6, A3, PARTFUN1:def_6
.= (R1 /. k) - (R2 /. k) by A1, A6, A3, VFUNCT_1:def_2 ; ::_thesis: verum
end;
thus  Sum R3 = (Sum R1) - (Sum R2) by A1, A4, A5, RLVECT_2:5; ::_thesis: verum
end;

theorem Th3: :: INTEGR18:3
for X being RealNormSpace
for R1, R2 being FinSequence of X
for a being Element of REAL st R2 = a (#) R1 holds
Sum R2 = a * (Sum R1)
proof
let X be RealNormSpace; ::_thesis: for R1, R2 being FinSequence of X
for a being Element of REAL st R2 = a (#) R1 holds
Sum R2 = a * (Sum R1)
let R1, R2 be FinSequence of X; ::_thesis: for a being Element of REAL st R2 = a (#) R1 holds
Sum R2 = a * (Sum R1)
let a be Element of REAL ; ::_thesis: ( R2 = a (#) R1 implies Sum R2 = a * (Sum R1) )
assume A1: R2 = a (#) R1 ; ::_thesis: Sum R2 = a * (Sum R1)
 dom R2 = dom R1 by A1, VFUNCT_1:def_4;
then A2: len R2 = len R1 by FINSEQ_3:29;
A3: for k being Element of NAT st k in dom R1 holds
R2 . k = a * (R1 /. k)
proof
let k be Element of NAT ; ::_thesis: ( k in dom R1 implies R2 . k = a * (R1 /. k) )
assume  k in dom R1 ; ::_thesis: R2 . k = a * (R1 /. k)
then A4: k in dom R2 by A1, VFUNCT_1:def_4;
thus R2 . k = R2 /. k by A4, PARTFUN1:def_6
.= a * (R1 /. k) by A4, A1, VFUNCT_1:def_4 ; ::_thesis: verum
end;
thus  Sum R2 = a * (Sum R1) by A2, A3, RLVECT_2:3; ::_thesis: verum
end;

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be Function of A, the carrier of X;
assume A1: f is integrable ;
func integral f ->  Point of X means :Def6: :: INTEGR18:def 6
 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)) = it );
existence
 ex b1 being Point of X st
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)) = b1 ) by A1, Def5;
uniqueness
 for b1, b2 being Point of X st ( 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)) = b1 ) ) & ( 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)) = b2 ) ) holds
b1 = b2
proof
let I1, I2 be Point of X; ::_thesis: ( ( 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)) = I1 ) ) & ( 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)) = I2 ) ) implies I1 = I2 )
assume 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)) = I1 ) ; ::_thesis: ( ex T being DivSequence of A ex S being middle_volume_Sequence of f,T st
( delta T is convergent & lim (delta T) = 0 & not ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I2 ) ) or I1 = I2 )
assume 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)) = I2 ) ; ::_thesis: I1 = I2
consider T being DivSequence of A such that
A4: ( delta T is convergent & lim (delta T) = 0 ) by INTEGRA4:11;
set S = the middle_volume_Sequence of f,T;
thus I1 = lim (middle_sum (f, the middle_volume_Sequence of f,T)) by A2, A4
.= I2 by A3, A4 ; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines integral INTEGR18:def_6_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X st f is integrable holds
for b4 being Point of X holds
( b4 = integral f iff 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)) = b4 ) );

theorem Th4: :: INTEGR18:4
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for r being Real
for f, h being Function of A, the carrier of X st h = r (#) f & f is integrable holds
( h is integrable & integral h = r * (integral f) )
proof
let X be RealNormSpace; ::_thesis: for A being non empty closed_interval Subset of REAL
for r being Real
for f, h being Function of A, the carrier of X st h = r (#) f & f is integrable holds
( h is integrable & integral h = r * (integral f) )
let A be non empty closed_interval Subset of REAL; ::_thesis: for r being Real
for f, h being Function of A, the carrier of X st h = r (#) f & f is integrable holds
( h is integrable & integral h = r * (integral f) )
let r be Real; ::_thesis: for f, h being Function of A, the carrier of X st h = r (#) f & f is integrable holds
( h is integrable & integral h = r * (integral f) )
let f, h be Function of A, the carrier of X; ::_thesis: ( h = r (#) f & f is integrable implies ( h is integrable & integral h = r * (integral f) ) )
assume A1: ( h = r (#) f & f is integrable ) ; ::_thesis: ( h is integrable & integral h = r * (integral f) )
A2: ( dom h = A & dom f = A ) by FUNCT_2:def_1;
A3: now__::_thesis:_for_T_being_DivSequence_of_A
for_S_being_middle_volume_Sequence_of_h,T_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_
(_middle_sum_(h,S)_is_convergent_&_lim_(middle_sum_(h,S))_=_r_*_(integral_f)_)
let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = r * (integral f) )
let S be middle_volume_Sequence of h,T; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = r * (integral f) ) )
assume A4: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = r * (integral f) )
defpred S1[ Element of NAT , set ] means  ex p being FinSequence of REAL st
( p = $2 & len p = len (T . $1) & ( for i being Nat st i in dom (T . $1) holds
( p . i in dom (h | (divset ((T . $1),i))) & ex z being Point of X st
( z = (h | (divset ((T . $1),i))) . (p . i) & (S . $1) . i = (vol (divset ((T . $1),i))) * z ) ) ) );
A5: for k being Element of NAT ex p being Element of REAL * st S1[k,p]
proof
let k be Element of NAT ; ::_thesis: ex p being Element of REAL * st S1[k,p]
defpred S2[ Nat, set ] means ( $2 in dom (h | (divset ((T . k),$1))) & ex c being Point of X st
( c = (h | (divset ((T . k),$1))) . $2 & (S . k) . $1 = (vol (divset ((T . k),$1))) * c ) );
A6: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def_3;
A7: for i being Nat st i in Seg (len (T . k)) holds
ex x being Element of REAL st S2[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S2[i,x] )
assume  i in Seg (len (T . k)) ; ::_thesis: ex x being Element of REAL st S2[i,x]
then  i in dom (T . k) by FINSEQ_1:def_3;
then consider c being Point of X such that
A8: ( c in rng (h | (divset ((T . k),i))) & (S . k) . i = (vol (divset ((T . k),i))) * c ) by Def1;
consider x being set  such that
A9: ( x in dom (h | (divset ((T . k),i))) & c = (h | (divset ((T . k),i))) . x ) by A8, FUNCT_1:def_3;
 ( x in dom h & x in divset ((T . k),i) ) by A9, RELAT_1:57;
then reconsider x = x as Element of REAL ;
take  x ; ::_thesis: S2[i,x]
thus  S2[i,x] by A8, A9; ::_thesis: verum
end;
consider p being FinSequence of REAL  such that
A10: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds
S2[i,p . i] ) ) from FINSEQ_1:sch_5(A7);
take  p ; ::_thesis: ( p is Element of REAL * & S1[k,p] )
 len p = len (T . k) by A10, FINSEQ_1:def_3;
hence  ( p is Element of REAL * & S1[k,p] ) by A10, A6, FINSEQ_1:def_11; ::_thesis: verum
end;
consider F being Function of NAT,(REAL *) such that
A11: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch_3(A5);
defpred S2[ Element of NAT , set ] means  ex q being middle_volume of f,T . $1 st
( q = $2 & ( for i being Nat st i in dom (T . $1) holds
ex z being Point of X st
( (F . $1) . i in dom (f | (divset ((T . $1),i))) & z = (f | (divset ((T . $1),i))) . ((F . $1) . i) & q . i = (vol (divset ((T . $1),i))) * z ) ) );
A12: for k being Element of NAT ex y being Element of the carrier of X * st S2[k,y]
proof
let k be Element of NAT ; ::_thesis: ex y being Element of the carrier of X * st S2[k,y]
defpred S3[ Nat, set ] means  ex c being Point of X st
( (F . k) . $1 in dom (f | (divset ((T . k),$1))) & c = (f | (divset ((T . k),$1))) . ((F . k) . $1) & $2 = (vol (divset ((T . k),$1))) * c );
A13: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def_3;
A14: for i being Nat st i in Seg (len (T . k)) holds
ex x being Element of the carrier of X st S3[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg (len (T . k)) implies ex x being Element of the carrier of X st S3[i,x] )
assume  i in Seg (len (T . k)) ; ::_thesis: ex x being Element of the carrier of X st S3[i,x]
then A15: i in dom (T . k) by FINSEQ_1:def_3;
consider p being FinSequence of REAL  such that
A16: ( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds
( p . i in dom (h | (divset ((T . k),i))) & ex z being Point of X st
( z = (h | (divset ((T . k),i))) . (p . i) & (S . k) . i = (vol (divset ((T . k),i))) * z ) ) ) ) by A11;
 p . i in dom (h | (divset ((T . k),i))) by A15, A16;
then A17: ( p . i in dom h & p . i in divset ((T . k),i) ) by RELAT_1:57;
then  p . i in dom (f | (divset ((T . k),i))) by A2, RELAT_1:57;
then  (f | (divset ((T . k),i))) . (p . i) in rng (f | (divset ((T . k),i))) by FUNCT_1:3;
then reconsider x = (f | (divset ((T . k),i))) . (p . i) as Element of the carrier of X ;
A18: (F . k) . i in dom (f | (divset ((T . k),i))) by A16, A17, A2, RELAT_1:57;
 (vol (divset ((T . k),i))) * x is Element of the carrier of X ;
hence  ex x being Element of the carrier of X st S3[i,x] by A16, A18; ::_thesis: verum
end;
consider q being FinSequence of the carrier of X such that
A19: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds
S3[i,q . i] ) ) from FINSEQ_1:sch_5(A14);
A20: len q = len (T . k) by A19, FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(T_._k)_holds_
ex_c_being_Point_of_X_st_
(_c_in_rng_(f_|_(divset_((T_._k),i)))_&_q_._i_=_(vol_(divset_((T_._k),i)))_*_c_)
let i be Nat; ::_thesis: ( i in dom (T . k) implies ex c being Point of X st
( c in rng (f | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) )
assume  i in dom (T . k) ; ::_thesis: ex c being Point of X st
( c in rng (f | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c )
then  i in Seg (len (T . k)) by FINSEQ_1:def_3;
then consider c being Point of X such that
A21: ( (F . k) . i in dom (f | (divset ((T . k),i))) & c = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * c ) by A19;
thus  ex c being Point of X st
( c in rng (f | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) by A21, FUNCT_1:3; ::_thesis: verum
end;
then reconsider q = q as middle_volume of f,T . k by A20, Def1;
 q is Element of the carrier of X * by FINSEQ_1:def_11;
hence  ex y being Element of the carrier of X * st S2[k,y] by A13, A19; ::_thesis: verum
end;
consider Sf being Function of NAT,( the carrier of X *) such that
A22: for x being Element of NAT holds S2[x,Sf . x] from FUNCT_2:sch_3(A12);
now__::_thesis:_for_k_being_Element_of_NAT_holds_Sf_._k_is_middle_volume_of_f,T_._k
let k be Element of NAT ; ::_thesis: Sf . k is middle_volume of f,T . k
 ex q being middle_volume of f,T . k st
( q = Sf . k & ( for i being Nat st i in dom (T . k) holds
ex z being Point of X st
( (F . k) . i in dom (f | (divset ((T . k),i))) & z = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * z ) ) ) by A22;
hence  Sf . k is middle_volume of f,T . k ; ::_thesis: verum
end;
then reconsider Sf = Sf as middle_volume_Sequence of f,T by Def3;
 integral f is Point of X ;
then A23: middle_sum (f,Sf) is convergent by Def6, A1, A4;
A24: r * (middle_sum (f,Sf)) = middle_sum (h,S)
proof
now__::_thesis:_for_n_being_Element_of_NAT_holds_r_*_((middle_sum_(f,Sf))_._n)_=_(middle_sum_(h,S))_._n
let n be Element of NAT ; ::_thesis: r * ((middle_sum (f,Sf)) . n) = (middle_sum (h,S)) . n
consider p being FinSequence of REAL  such that
A25: ( p = F . n & len p = len (T . n) & ( for i being Nat st i in dom (T . n) holds
( p . i in dom (h | (divset ((T . n),i))) & ex z being Point of X st
( z = (h | (divset ((T . n),i))) . (p . i) & (S . n) . i = (vol (divset ((T . n),i))) * z ) ) ) ) by A11;
consider q being middle_volume of f,T . n such that
A26: ( q = Sf . n & ( for i being Nat st i in dom (T . n) holds
ex z being Point of X st
( (F . n) . i in dom (f | (divset ((T . n),i))) & z = (f | (divset ((T . n),i))) . ((F . n) . i) & q . i = (vol (divset ((T . n),i))) * z ) ) ) by A22;
 ( len (Sf . n) = len (T . n) & len (S . n) = len (T . n) ) by Def1;
then A27: ( dom (Sf . n) = dom (T . n) & dom (S . n) = dom (T . n) ) by FINSEQ_3:29;
now__::_thesis:_for_x_being_Element_of_NAT_st_x_in_dom_(S_._n)_holds_
(S_._n)_/._x_=_r_*_((Sf_._n)_/._x)
let x be Element of NAT ; ::_thesis: ( x in dom (S . n) implies (S . n) /. x = r * ((Sf . n) /. x) )
assume A28: x in dom (S . n) ; ::_thesis: (S . n) /. x = r * ((Sf . n) /. x)
reconsider i = x as Nat ;
consider t being Point of X such that
A29: ( t = (h | (divset ((T . n),i))) . ((F . n) . i) & (S . n) . i = (vol (divset ((T . n),i))) * t ) by A28, A27, A25;
consider z being Point of X such that
A30: ( (F . n) . i in dom (f | (divset ((T . n),i))) & z = (f | (divset ((T . n),i))) . ((F . n) . i) & q . i = (vol (divset ((T . n),i))) * z ) by A26, A28, A27;
A31: (F . n) . i in divset ((T . n),i) by A30, RELAT_1:57;
 (F . n) . i in A by A30;
then A32: (F . n) . i in dom h by FUNCT_2:def_1;
A33: (F . n) . i in dom f by A30, RELAT_1:57;
A34: f /. ((F . n) . i) = f . ((F . n) . i) by A33, PARTFUN1:def_6
.= z by A30, A31, FUNCT_1:49 ;
A35: t = (h | (divset ((T . n),i))) . ((F . n) . i) by A29
.= h . ((F . n) . i) by A31, FUNCT_1:49
.= h /. ((F . n) . i) by A32, PARTFUN1:def_6
.= r * (f /. ((F . n) . i)) by A32, A1, VFUNCT_1:def_4
.= r * z by A34 ;
A36: (vol (divset ((T . n),i))) * z = (Sf . n) . x by A30, A26
.= (Sf . n) /. x by A28, A27, PARTFUN1:def_6 ;
thus (S . n) /. x = (S . n) . x by A28, PARTFUN1:def_6
.= (vol (divset ((T . n),i))) * t by A29
.= (vol (divset ((T . n),i))) * (r * z) by A35
.= ((vol (divset ((T . n),i))) * r) * z by RLVECT_1:def_7
.= r * ((vol (divset ((T . n),i))) * z) by RLVECT_1:def_7
.= r * ((Sf . n) /. x) by A36 ; ::_thesis: verum
end;
then A37: r (#) (Sf . n) = S . n by A27, VFUNCT_1:def_4;
thus r * ((middle_sum (f,Sf)) . n) = r * (middle_sum (f,(Sf . n))) by Def4
.= r * (Sum (Sf . n))
.= Sum (S . n) by A37, Th3
.= middle_sum (h,(S . n))
.= (middle_sum (h,S)) . n by Def4 ; ::_thesis: verum
end;
hence  r * (middle_sum (f,Sf)) = middle_sum (h,S) by NORMSP_1:def_5; ::_thesis: verum
end;
A38: lim (r * (middle_sum (f,Sf))) = r * (lim (middle_sum (f,Sf))) by A23, NORMSP_1:28
.= r * (integral f) by Def6, A1, A4 ;
thus  middle_sum (h,S) is convergent by A23, A24, NORMSP_1:22; ::_thesis: lim (middle_sum (h,S)) = r * (integral f)
thus  lim (middle_sum (h,S)) = r * (integral f) by A24, A38; ::_thesis: verum
end;
hence  h is integrable by Def5; ::_thesis: integral h = r * (integral f)
hence  integral h = r * (integral f) by Def6, A3; ::_thesis: verum
end;

theorem Th5: :: INTEGR18:5
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f, h being Function of A, the carrier of X st h = - f & f is integrable holds
( h is integrable & integral h = - (integral f) )
proof
let X be RealNormSpace; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, h being Function of A, the carrier of X st h = - f & f is integrable holds
( h is integrable & integral h = - (integral f) )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, h being Function of A, the carrier of X st h = - f & f is integrable holds
( h is integrable & integral h = - (integral f) )
let f, h be Function of A, the carrier of X; ::_thesis: ( h = - f & f is integrable implies ( h is integrable & integral h = - (integral f) ) )
assume A1: ( h = - f & f is integrable ) ; ::_thesis: ( h is integrable & integral h = - (integral f) )
then A2: h = (- 1) (#) f by VFUNCT_1:23;
hence  h is integrable by A1, Th4; ::_thesis: integral h = - (integral f)
 integral h = (- 1) * (integral f) by A1, A2, Th4;
hence  integral h = - (integral f) by RLVECT_1:16; ::_thesis: verum
end;

theorem Th6: :: INTEGR18:6
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f, g, h being Function of A, the carrier of X st h = f + g & f is integrable & g is integrable holds
( h is integrable & integral h = (integral f) + (integral g) )
proof
let X be RealNormSpace; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, g, h being Function of A, the carrier of X st h = f + g & f is integrable & g is integrable holds
( h is integrable & integral h = (integral f) + (integral g) )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g, h being Function of A, the carrier of X st h = f + g & f is integrable & g is integrable holds
( h is integrable & integral h = (integral f) + (integral g) )
let f, g, h be Function of A, the carrier of X; ::_thesis: ( h = f + g & f is integrable & g is integrable implies ( h is integrable & integral h = (integral f) + (integral g) ) )
assume A1: ( h = f + g & f is integrable & g is integrable ) ; ::_thesis: ( h is integrable & integral h = (integral f) + (integral g) )
A2: ( dom h = A & dom f = A & dom g = A ) by FUNCT_2:def_1;
A3: now__::_thesis:_for_T_being_DivSequence_of_A
for_S_being_middle_volume_Sequence_of_h,T_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_
(_middle_sum_(h,S)_is_convergent_&_lim_(middle_sum_(h,S))_=_(integral_f)_+_(integral_g)_)
let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = (integral f) + (integral g) )
let S be middle_volume_Sequence of h,T; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = (integral f) + (integral g) ) )
assume A4: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = (integral f) + (integral g) )
defpred S1[ Element of NAT , set ] means  ex p being FinSequence of REAL st
( p = $2 & len p = len (T . $1) & ( for i being Nat st i in dom (T . $1) holds
( p . i in dom (h | (divset ((T . $1),i))) & ex z being Point of X st
( z = (h | (divset ((T . $1),i))) . (p . i) & (S . $1) . i = (vol (divset ((T . $1),i))) * z ) ) ) );
A5: for k being Element of NAT ex p being Element of REAL * st S1[k,p]
proof
let k be Element of NAT ; ::_thesis: ex p being Element of REAL * st S1[k,p]
defpred S2[ Nat, set ] means ( $2 in dom (h | (divset ((T . k),$1))) & ex c being Point of X st
( c = (h | (divset ((T . k),$1))) . $2 & (S . k) . $1 = (vol (divset ((T . k),$1))) * c ) );
A6: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def_3;
A7: for i being Nat st i in Seg (len (T . k)) holds
ex x being Element of REAL st S2[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S2[i,x] )
assume  i in Seg (len (T . k)) ; ::_thesis: ex x being Element of REAL st S2[i,x]
then  i in dom (T . k) by FINSEQ_1:def_3;
then consider c being Point of X such that
A8: ( c in rng (h | (divset ((T . k),i))) & (S . k) . i = (vol (divset ((T . k),i))) * c ) by Def1;
consider x being set  such that
A9: ( x in dom (h | (divset ((T . k),i))) & c = (h | (divset ((T . k),i))) . x ) by A8, FUNCT_1:def_3;
 ( x in dom h & x in divset ((T . k),i) ) by A9, RELAT_1:57;
then reconsider x = x as Element of REAL ;
take  x ; ::_thesis: S2[i,x]
thus  S2[i,x] by A8, A9; ::_thesis: verum
end;
consider p being FinSequence of REAL  such that
A10: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds
S2[i,p . i] ) ) from FINSEQ_1:sch_5(A7);
take  p ; ::_thesis: ( p is Element of REAL * & S1[k,p] )
 len p = len (T . k) by A10, FINSEQ_1:def_3;
hence  ( p is Element of REAL * & S1[k,p] ) by A10, A6, FINSEQ_1:def_11; ::_thesis: verum
end;
consider F being Function of NAT,(REAL *) such that
A11: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch_3(A5);
defpred S2[ Element of NAT , set ] means  ex q being middle_volume of f,T . $1 st
( q = $2 & ( for i being Nat st i in dom (T . $1) holds
ex z being Point of X st
( (F . $1) . i in dom (f | (divset ((T . $1),i))) & z = (f | (divset ((T . $1),i))) . ((F . $1) . i) & q . i = (vol (divset ((T . $1),i))) * z ) ) );
A12: for k being Element of NAT ex y being Element of the carrier of X * st S2[k,y]
proof
let k be Element of NAT ; ::_thesis: ex y being Element of the carrier of X * st S2[k,y]
defpred S3[ Nat, set ] means  ex c being Point of X st
( (F . k) . $1 in dom (f | (divset ((T . k),$1))) & c = (f | (divset ((T . k),$1))) . ((F . k) . $1) & $2 = (vol (divset ((T . k),$1))) * c );
A13: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def_3;
A14: for i being Nat st i in Seg (len (T . k)) holds
ex x being Element of the carrier of X st S3[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg (len (T . k)) implies ex x being Element of the carrier of X st S3[i,x] )
assume  i in Seg (len (T . k)) ; ::_thesis: ex x being Element of the carrier of X st S3[i,x]
then A15: i in dom (T . k) by FINSEQ_1:def_3;
consider p being FinSequence of REAL  such that
A16: ( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds
( p . i in dom (h | (divset ((T . k),i))) & ex z being Point of X st
( z = (h | (divset ((T . k),i))) . (p . i) & (S . k) . i = (vol (divset ((T . k),i))) * z ) ) ) ) by A11;
 p . i in dom (h | (divset ((T . k),i))) by A15, A16;
then A17: ( p . i in dom h & p . i in divset ((T . k),i) ) by RELAT_1:57;
then  p . i in dom (f | (divset ((T . k),i))) by A2, RELAT_1:57;
then  (f | (divset ((T . k),i))) . (p . i) in rng (f | (divset ((T . k),i))) by FUNCT_1:3;
then reconsider x = (f | (divset ((T . k),i))) . (p . i) as Element of the carrier of X ;
A18: (F . k) . i in dom (f | (divset ((T . k),i))) by A16, A17, A2, RELAT_1:57;
 (vol (divset ((T . k),i))) * x is Element of the carrier of X ;
hence  ex x being Element of the carrier of X st S3[i,x] by A16, A18; ::_thesis: verum
end;
consider q being FinSequence of the carrier of X such that
A19: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds
S3[i,q . i] ) ) from FINSEQ_1:sch_5(A14);
A20: len q = len (T . k) by A19, FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(T_._k)_holds_
ex_c_being_Point_of_X_st_
(_c_in_rng_(f_|_(divset_((T_._k),i)))_&_q_._i_=_(vol_(divset_((T_._k),i)))_*_c_)
let i be Nat; ::_thesis: ( i in dom (T . k) implies ex c being Point of X st
( c in rng (f | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) )
assume  i in dom (T . k) ; ::_thesis: ex c being Point of X st
( c in rng (f | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c )
then  i in Seg (len (T . k)) by FINSEQ_1:def_3;
then consider c being Point of X such that
A21: ( (F . k) . i in dom (f | (divset ((T . k),i))) & c = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * c ) by A19;
thus  ex c being Point of X st
( c in rng (f | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) by A21, FUNCT_1:3; ::_thesis: verum
end;
then reconsider q = q as middle_volume of f,T . k by A20, Def1;
 q is Element of the carrier of X * by FINSEQ_1:def_11;
hence  ex y being Element of the carrier of X * st S2[k,y] by A13, A19; ::_thesis: verum
end;
consider Sf being Function of NAT,( the carrier of X *) such that
A22: for x being Element of NAT holds S2[x,Sf . x] from FUNCT_2:sch_3(A12);
now__::_thesis:_for_k_being_Element_of_NAT_holds_Sf_._k_is_middle_volume_of_f,T_._k
let k be Element of NAT ; ::_thesis: Sf . k is middle_volume of f,T . k
 ex q being middle_volume of f,T . k st
( q = Sf . k & ( for i being Nat st i in dom (T . k) holds
ex z being Point of X st
( (F . k) . i in dom (f | (divset ((T . k),i))) & z = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * z ) ) ) by A22;
hence  Sf . k is middle_volume of f,T . k ; ::_thesis: verum
end;
then reconsider Sf = Sf as middle_volume_Sequence of f,T by Def3;
defpred S3[ Element of NAT , set ] means  ex q being middle_volume of g,T . $1 st
( q = $2 & ( for i being Nat st i in dom (T . $1) holds
ex z being Point of X st
( (F . $1) . i in dom (g | (divset ((T . $1),i))) & z = (g | (divset ((T . $1),i))) . ((F . $1) . i) & q . i = (vol (divset ((T . $1),i))) * z ) ) );
A23: for k being Element of NAT ex y being Element of the carrier of X * st S3[k,y]
proof
let k be Element of NAT ; ::_thesis: ex y being Element of the carrier of X * st S3[k,y]
defpred S4[ Nat, set ] means  ex c being Point of X st
( (F . k) . $1 in dom (g | (divset ((T . k),$1))) & c = (g | (divset ((T . k),$1))) . ((F . k) . $1) & $2 = (vol (divset ((T . k),$1))) * c );
A24: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def_3;
A25: for i being Nat st i in Seg (len (T . k)) holds
ex x being Element of the carrier of X st S4[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg (len (T . k)) implies ex x being Element of the carrier of X st S4[i,x] )
assume  i in Seg (len (T . k)) ; ::_thesis: ex x being Element of the carrier of X st S4[i,x]
then A26: i in dom (T . k) by FINSEQ_1:def_3;
consider p being FinSequence of REAL  such that
A27: ( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds
( p . i in dom (h | (divset ((T . k),i))) & ex z being Point of X st
( z = (h | (divset ((T . k),i))) . (p . i) & (S . k) . i = (vol (divset ((T . k),i))) * z ) ) ) ) by A11;
 p . i in dom (h | (divset ((T . k),i))) by A26, A27;
then A28: ( p . i in dom h & p . i in divset ((T . k),i) ) by RELAT_1:57;
then  p . i in dom (g | (divset ((T . k),i))) by A2, RELAT_1:57;
then  (g | (divset ((T . k),i))) . (p . i) in rng (g | (divset ((T . k),i))) by FUNCT_1:3;
then reconsider x = (g | (divset ((T . k),i))) . (p . i) as Element of the carrier of X ;
A29: (F . k) . i in dom (g | (divset ((T . k),i))) by A27, A28, A2, RELAT_1:57;
 (vol (divset ((T . k),i))) * x is Element of the carrier of X ;
hence  ex x being Element of the carrier of X st S4[i,x] by A27, A29; ::_thesis: verum
end;
consider q being FinSequence of the carrier of X such that
A30: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds
S4[i,q . i] ) ) from FINSEQ_1:sch_5(A25);
A31: len q = len (T . k) by A30, FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(T_._k)_holds_
ex_c_being_Point_of_X_st_
(_c_in_rng_(g_|_(divset_((T_._k),i)))_&_q_._i_=_(vol_(divset_((T_._k),i)))_*_c_)
let i be Nat; ::_thesis: ( i in dom (T . k) implies ex c being Point of X st
( c in rng (g | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) )
assume  i in dom (T . k) ; ::_thesis: ex c being Point of X st
( c in rng (g | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c )
then  i in Seg (len (T . k)) by FINSEQ_1:def_3;
then consider c being Point of X such that
A32: ( (F . k) . i in dom (g | (divset ((T . k),i))) & c = (g | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * c ) by A30;
thus  ex c being Point of X st
( c in rng (g | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) by A32, FUNCT_1:3; ::_thesis: verum
end;
then reconsider q = q as middle_volume of g,T . k by A31, Def1;
 q is Element of the carrier of X * by FINSEQ_1:def_11;
hence  ex y being Element of the carrier of X * st S3[k,y] by A24, A30; ::_thesis: verum
end;
consider Sg being Function of NAT,( the carrier of X *) such that
A33: for x being Element of NAT holds S3[x,Sg . x] from FUNCT_2:sch_3(A23);
now__::_thesis:_for_k_being_Element_of_NAT_holds_Sg_._k_is_middle_volume_of_g,T_._k
let k be Element of NAT ; ::_thesis: Sg . k is middle_volume of g,T . k
 ex q being middle_volume of g,T . k st
( q = Sg . k & ( for i being Nat st i in dom (T . k) holds
ex z being Point of X st
( (F . k) . i in dom (g | (divset ((T . k),i))) & z = (g | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * z ) ) ) by A33;
hence  Sg . k is middle_volume of g,T . k ; ::_thesis: verum
end;
then reconsider Sg = Sg as middle_volume_Sequence of g,T by Def3;
 integral f is Point of X ;
then A34: ( middle_sum (f,Sf) is convergent & lim (middle_sum (f,Sf)) = integral f ) by Def6, A1, A4;
 integral g is Point of X ;
then A35: ( middle_sum (g,Sg) is convergent & lim (middle_sum (g,Sg)) = integral g ) by Def6, A1, A4;
A36: (middle_sum (f,Sf)) + (middle_sum (g,Sg)) = middle_sum (h,S)
proof
now__::_thesis:_for_n_being_Element_of_NAT_holds_((middle_sum_(f,Sf))_._n)_+_((middle_sum_(g,Sg))_._n)_=_(middle_sum_(h,S))_._n
let n be Element of NAT ; ::_thesis: ((middle_sum (f,Sf)) . n) + ((middle_sum (g,Sg)) . n) = (middle_sum (h,S)) . n
consider p being FinSequence of REAL  such that
A37: ( p = F . n & len p = len (T . n) & ( for i being Nat st i in dom (T . n) holds
( p . i in dom (h | (divset ((T . n),i))) & ex z being Point of X st
( z = (h | (divset ((T . n),i))) . (p . i) & (S . n) . i = (vol (divset ((T . n),i))) * z ) ) ) ) by A11;
consider q being middle_volume of f,T . n such that
A38: ( q = Sf . n & ( for i being Nat st i in dom (T . n) holds
ex z being Point of X st
( (F . n) . i in dom (f | (divset ((T . n),i))) & z = (f | (divset ((T . n),i))) . ((F . n) . i) & q . i = (vol (divset ((T . n),i))) * z ) ) ) by A22;
consider r being middle_volume of g,T . n such that
A39: ( r = Sg . n & ( for i being Nat st i in dom (T . n) holds
ex z being Point of X st
( (F . n) . i in dom (g | (divset ((T . n),i))) & z = (g | (divset ((T . n),i))) . ((F . n) . i) & r . i = (vol (divset ((T . n),i))) * z ) ) ) by A33;
A40: ( len (Sf . n) = len (T . n) & len (Sg . n) = len (T . n) & len (S . n) = len (T . n) ) by Def1;
A41: ( dom (Sf . n) = dom (T . n) & dom (Sg . n) = dom (T . n) & dom (S . n) = dom (T . n) ) by A40, FINSEQ_3:29;
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(S_._n)_holds_
(S_._n)_/._i_=_((Sf_._n)_/._i)_+_((Sg_._n)_/._i)
let i be Nat; ::_thesis: ( 1 <= i & i <= len (S . n) implies (S . n) /. i = ((Sf . n) /. i) + ((Sg . n) /. i) )
assume  ( 1 <= i & i <= len (S . n) ) ; ::_thesis: (S . n) /. i = ((Sf . n) /. i) + ((Sg . n) /. i)
then  i in Seg (len (S . n)) by FINSEQ_1:1;
then A42: i in dom (S . n) by FINSEQ_1:def_3;
consider t being Point of X such that
A43: ( t = (h | (divset ((T . n),i))) . ((F . n) . i) & (S . n) . i = (vol (divset ((T . n),i))) * t ) by A42, A41, A37;
consider z being Point of X such that
A44: ( (F . n) . i in dom (f | (divset ((T . n),i))) & z = (f | (divset ((T . n),i))) . ((F . n) . i) & q . i = (vol (divset ((T . n),i))) * z ) by A38, A42, A41;
consider w being Point of X such that
A45: ( (F . n) . i in dom (g | (divset ((T . n),i))) & w = (g | (divset ((T . n),i))) . ((F . n) . i) & r . i = (vol (divset ((T . n),i))) * w ) by A39, A42, A41;
A46: (F . n) . i in divset ((T . n),i) by A45, RELAT_1:57;
A47: (F . n) . i in dom g by A45, RELAT_1:57;
A48: (F . n) . i in A by A45;
then A49: (F . n) . i in dom h by FUNCT_2:def_1;
A50: (F . n) . i in dom f by A48, FUNCT_2:def_1;
A51: f /. ((F . n) . i) = f . ((F . n) . i) by A50, PARTFUN1:def_6
.= z by A44, A46, FUNCT_1:49 ;
A52: g /. ((F . n) . i) = g . ((F . n) . i) by A47, PARTFUN1:def_6
.= w by A45, A46, FUNCT_1:49 ;
A53: t = (h | (divset ((T . n),i))) . ((F . n) . i) by A43
.= h . ((F . n) . i) by A46, FUNCT_1:49
.= h /. ((F . n) . i) by A49, PARTFUN1:def_6
.= (f /. ((F . n) . i)) + (g /. ((F . n) . i)) by A49, A1, VFUNCT_1:def_1
.= z + w by A51, A52 ;
A54: (vol (divset ((T . n),i))) * z = (Sf . n) . i by A44, A38
.= (Sf . n) /. i by A42, A41, PARTFUN1:def_6 ;
A55: (vol (divset ((T . n),i))) * w = (Sg . n) . i by A45, A39
.= (Sg . n) /. i by A42, A41, PARTFUN1:def_6 ;
thus (S . n) /. i = (S . n) . i by A42, PARTFUN1:def_6
.= (vol (divset ((T . n),i))) * t by A43
.= ((vol (divset ((T . n),i))) * z) + ((vol (divset ((T . n),i))) * w) by A53, RLVECT_1:def_5
.= ((Sf . n) /. i) + ((Sg . n) /. i) by A54, A55 ; ::_thesis: verum
end;
then A56: (Sf . n) + (Sg . n) = S . n by A41, BINOM:def_1;
thus ((middle_sum (f,Sf)) . n) + ((middle_sum (g,Sg)) . n) = (middle_sum (f,(Sf . n))) + ((middle_sum (g,Sg)) . n) by Def4
.= (middle_sum (f,(Sf . n))) + (middle_sum (g,(Sg . n))) by Def4
.= (Sum (Sf . n)) + (middle_sum (g,(Sg . n)))
.= (Sum (Sf . n)) + (Sum (Sg . n))
.= Sum (S . n) by A56, A40, Th1
.= middle_sum (h,(S . n))
.= (middle_sum (h,S)) . n by Def4 ; ::_thesis: verum
end;
hence  (middle_sum (f,Sf)) + (middle_sum (g,Sg)) = middle_sum (h,S) by NORMSP_1:def_2; ::_thesis: verum
end;
hence  middle_sum (h,S) is convergent by A34, A35, NORMSP_1:19; ::_thesis: lim (middle_sum (h,S)) = (integral f) + (integral g)
thus  lim (middle_sum (h,S)) = (integral f) + (integral g) by A34, A35, A36, NORMSP_1:25; ::_thesis: verum
end;
hence  h is integrable by Def5; ::_thesis: integral h = (integral f) + (integral g)
hence  integral h = (integral f) + (integral g) by Def6, A3; ::_thesis: verum
end;

theorem :: INTEGR18:7
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f, g, h being Function of A, the carrier of X st h = f - g & f is integrable & g is integrable holds
( h is integrable & integral h = (integral f) - (integral g) )
proof
let X be RealNormSpace; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, g, h being Function of A, the carrier of X st h = f - g & f is integrable & g is integrable holds
( h is integrable & integral h = (integral f) - (integral g) )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g, h being Function of A, the carrier of X st h = f - g & f is integrable & g is integrable holds
( h is integrable & integral h = (integral f) - (integral g) )
let f, g, h be Function of A, the carrier of X; ::_thesis: ( h = f - g & f is integrable & g is integrable implies ( h is integrable & integral h = (integral f) - (integral g) ) )
assume A1: ( h = f - g & f is integrable & g is integrable ) ; ::_thesis: ( h is integrable & integral h = (integral f) - (integral g) )
then A2: h = f + (- g) by VFUNCT_1:25;
dom (- g) = dom g by VFUNCT_1:def_5
.= A by FUNCT_2:def_1 ;
then reconsider gg = - g as Function of A, the carrier of X by FUNCT_2:def_1;
A3: gg is integrable by A1, Th5;
hence  h is integrable by A1, A2, Th6; ::_thesis: integral h = (integral f) - (integral g)
 integral h = (integral f) + (integral gg) by A1, A2, A3, Th6;
then  integral h = (integral f) + (- (integral g)) by A1, Th5;
hence  integral h = (integral f) - (integral g) by RLVECT_1:def_11; ::_thesis: verum
end;

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL, the carrier of X;
predf is_integrable_on A means :Def7: :: INTEGR18:def 7
 ex g being Function of A, the carrier of X st
( g = f | A & g is integrable );
end;

:: deftheorem Def7 defines is_integrable_on INTEGR18:def_7_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X holds
( f is_integrable_on A iff ex g being Function of A, the carrier of X st
( g = f | A & g is integrable ) );

definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL, the carrier of X;
assume A1: A c= dom f ;
func integral (f,A) ->  Element of X means :Def8: :: INTEGR18:def 8
 ex g being Function of A, the carrier of X st
( g = f | A & it = integral g );
correctness
existence
ex b1 being Element of X ex g being Function of A, the carrier of X st
( g = f | A & b1 = integral g );
uniqueness
for b1, b2 being Element of X st ex g being Function of A, the carrier of X st
( g = f | A & b1 = integral g ) & ex g being Function of A, the carrier of X st
( g = f | A & b2 = integral g ) holds
b1 = b2;
proof
A2: dom (f | A) = A by A1, RELAT_1:62;
 rng (f | A) c= the carrier of X ;
then reconsider g = f | A as Function of A, the carrier of X by A2, FUNCT_2:2;
 integral g is Point of X ;
hence  ( ex b1 being Element of X ex g being Function of A, the carrier of X st
( g = f | A & b1 = integral g ) & ( for b1, b2 being Element of X st ex g being Function of A, the carrier of X st
( g = f | A & b1 = integral g ) & ex g being Function of A, the carrier of X st
( g = f | A & b2 = integral g ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines integral INTEGR18:def_8_:_
 for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X st A c= dom f holds
for b4 being Element of X holds
( b4 = integral (f,A) iff ex g being Function of A, the carrier of X st
( g = f | A & b4 = integral g ) );

theorem Th8: :: INTEGR18:8
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X
for g being Function of A, the carrier of X st f | A = g holds
( f is_integrable_on A iff g is integrable )
proof
let X be RealNormSpace; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X
for g being Function of A, the carrier of X st f | A = g holds
( f is_integrable_on A iff g is integrable )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL, the carrier of X
for g being Function of A, the carrier of X st f | A = g holds
( f is_integrable_on A iff g is integrable )
let f be PartFunc of REAL, the carrier of X; ::_thesis: for g being Function of A, the carrier of X st f | A = g holds
( f is_integrable_on A iff g is integrable )
let g be Function of A, the carrier of X; ::_thesis: ( f | A = g implies ( f is_integrable_on A iff g is integrable ) )
assume A1: f | A = g ; ::_thesis: ( f is_integrable_on A iff g is integrable )
hereby  ::_thesis: ( g is integrable implies f is_integrable_on A )
assume  f is_integrable_on A ; ::_thesis: g is integrable
then  ex g being Function of A, the carrier of X st
( g = f | A & g is integrable ) by Def7;
hence  g is integrable by A1; ::_thesis: verum
end;
assume  g is integrable ; ::_thesis: f is_integrable_on A
hence  f is_integrable_on A by A1, Def7; ::_thesis: verum
end;

theorem :: INTEGR18:9
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X
for g being Function of A, the carrier of X st A c= dom f & f | A = g holds
integral (f,A) = integral g by Def8;

theorem Th10: :: INTEGR18:10
for X, Y being non empty set
for V being RealNormSpace
for g, f being PartFunc of X, the carrier of V
for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds
g1 + f1 = g + f
proof
let X, Y be non empty set ; ::_thesis: for V being RealNormSpace
for g, f being PartFunc of X, the carrier of V
for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds
g1 + f1 = g + f
let V be RealNormSpace; ::_thesis: for g, f being PartFunc of X, the carrier of V
for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds
g1 + f1 = g + f
let g, f be PartFunc of X, the carrier of V; ::_thesis: for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds
g1 + f1 = g + f
let g1, f1 be PartFunc of Y, the carrier of V; ::_thesis: ( g = g1 & f = f1 implies g1 + f1 = g + f )
assume A1: ( g = g1 & f = f1 ) ; ::_thesis: g1 + f1 = g + f
A2: dom (g + f) = (dom g) /\ (dom f) by VFUNCT_1:def_1
.= (dom g1) /\ (dom f1) by A1 ;
A3: g + f is PartFunc of Y, the carrier of V by A2, RELSET_1:5;
 for c being Element of Y st c in dom (g + f) holds
(g + f) /. c = (g1 /. c) + (f1 /. c) by A1, VFUNCT_1:def_1;
hence  g1 + f1 = g + f by A3, A2, VFUNCT_1:def_1; ::_thesis: verum
end;

theorem :: INTEGR18:11
for X, Y being non empty set
for V being RealNormSpace
for g, f being PartFunc of X, the carrier of V
for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds
g1 - f1 = g - f
proof
let X, Y be non empty set ; ::_thesis: for V being RealNormSpace
for g, f being PartFunc of X, the carrier of V
for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds
g1 - f1 = g - f
let V be RealNormSpace; ::_thesis: for g, f being PartFunc of X, the carrier of V
for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds
g1 - f1 = g - f
let g, f be PartFunc of X, the carrier of V; ::_thesis: for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds
g1 - f1 = g - f
let g1, f1 be PartFunc of Y, the carrier of V; ::_thesis: ( g = g1 & f = f1 implies g1 - f1 = g - f )
assume A1: ( g = g1 & f = f1 ) ; ::_thesis: g1 - f1 = g - f
A2: dom (g - f) = (dom g) /\ (dom f) by VFUNCT_1:def_2
.= (dom g1) /\ (dom f1) by A1 ;
A3: g - f is PartFunc of Y, the carrier of V by A2, RELSET_1:5;
 for c being Element of Y st c in dom (g - f) holds
(g - f) /. c = (g1 /. c) - (f1 /. c) by A1, VFUNCT_1:def_2;
hence  g1 - f1 = g - f by A3, A2, VFUNCT_1:def_2; ::_thesis: verum
end;

theorem Th12: :: INTEGR18:12
for r being Real
for X, Y being non empty set
for V being RealNormSpace
for g being PartFunc of X, the carrier of V
for g1 being PartFunc of Y, the carrier of V st g = g1 holds
r (#) g1 = r (#) g
proof
let r be Real; ::_thesis: for X, Y being non empty set
for V being RealNormSpace
for g being PartFunc of X, the carrier of V
for g1 being PartFunc of Y, the carrier of V st g = g1 holds
r (#) g1 = r (#) g
let X, Y be non empty set ; ::_thesis: for V being RealNormSpace
for g being PartFunc of X, the carrier of V
for g1 being PartFunc of Y, the carrier of V st g = g1 holds
r (#) g1 = r (#) g
let V be RealNormSpace; ::_thesis: for g being PartFunc of X, the carrier of V
for g1 being PartFunc of Y, the carrier of V st g = g1 holds
r (#) g1 = r (#) g
let g be PartFunc of X, the carrier of V; ::_thesis: for g1 being PartFunc of Y, the carrier of V st g = g1 holds
r (#) g1 = r (#) g
let g1 be PartFunc of Y, the carrier of V; ::_thesis: ( g = g1 implies r (#) g1 = r (#) g )
assume A1: g = g1 ; ::_thesis: r (#) g1 = r (#) g
A2: dom (r (#) g) = dom g by VFUNCT_1:def_4
.= dom g1 by A1 ;
A3: r (#) g is PartFunc of Y, the carrier of V by A2, RELSET_1:5;
 for c being Element of Y st c in dom (r (#) g) holds
(r (#) g) /. c = r * (g1 /. c) by A1, VFUNCT_1:def_4;
hence  r (#) g1 = r (#) g by A3, A2, VFUNCT_1:def_4; ::_thesis: verum
end;

begin

theorem Th13: :: INTEGR18:13
for X being RealNormSpace
for r being Real
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X st A c= dom f & f is_integrable_on A holds
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
proof
let X be RealNormSpace; ::_thesis: for r being Real
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X st A c= dom f & f is_integrable_on A holds
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of X st A c= dom f & f is_integrable_on A holds
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL, the carrier of X st A c= dom f & f is_integrable_on A holds
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
let f be PartFunc of REAL, the carrier of X; ::_thesis: ( A c= dom f & f is_integrable_on A implies ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) )
assume A1: ( A c= dom f & f is_integrable_on A ) ; ::_thesis: ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
A2: A c= dom (r (#) f) by A1, VFUNCT_1:def_4;
consider g being Function of A, the carrier of X such that
A3: ( g = f | A & g is integrable ) by A1, Def7;
A4: (r (#) f) | A = r (#) (f | A) by VFUNCT_1:31
.= r (#) g by A3, Th12 ;
 r (#) g is total by VFUNCT_1:34;
then reconsider gg = r (#) g as Function of A, the carrier of X ;
 ( gg is integrable & integral gg = r * (integral g) ) by A3, Th4;
hence  r (#) f is_integrable_on A by A4, Th8; ::_thesis: integral ((r (#) f),A) = r * (integral (f,A))
thus  integral ((r (#) f),A) = integral gg by A4, A2, Def8
.= r * (integral g) by A3, Th4
.= r * (integral (f,A)) by A3, A1, Def8 ; ::_thesis: verum
end;

theorem Th14: :: INTEGR18:14
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds
( f1 + f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) )
proof
let X be RealNormSpace; ::_thesis: for A being non empty closed_interval Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds
( f1 + f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds
( f1 + f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) )
let f1, f2 be PartFunc of REAL, the carrier of X; ::_thesis: ( f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 implies ( f1 + f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) ) )
assume that
A1: ( f1 is_integrable_on A & f2 is_integrable_on A ) and
A2: ( A c= dom f1 & A c= dom f2 ) ; ::_thesis: ( f1 + f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) )
 A c= (dom f1) /\ (dom f2) by A2, XBOOLE_1:19;
then A3: A c= dom (f1 + f2) by VFUNCT_1:def_1;
consider g1 being Function of A, the carrier of X such that
A4: ( g1 = f1 | A & g1 is integrable ) by A1, Def7;
consider g2 being Function of A, the carrier of X such that
A5: ( g2 = f2 | A & g2 is integrable ) by A1, Def7;
 (f1 + f2) | A = (f1 | A) + (f2 | A) by VFUNCT_1:27;
then A6: (f1 + f2) | A = g1 + g2 by A4, A5, Th10;
 g1 + g2 is total by VFUNCT_1:32;
then reconsider g = g1 + g2 as Function of A, the carrier of X ;
 g is integrable by Th6, A4, A5;
hence  f1 + f2 is_integrable_on A by A6, Th8; ::_thesis: integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A))
thus  integral ((f1 + f2),A) = integral g by Def8, A6, A3
.= (integral g1) + (integral g2) by Th6, A4, A5
.= (integral (f1,A)) + (integral g2) by A2, A4, Def8
.= (integral (f1,A)) + (integral (f2,A)) by A2, A5, Def8 ; ::_thesis: verum
end;

theorem :: INTEGR18:15
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds
( f1 - f2 is_integrable_on A & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
proof
let X be RealNormSpace; ::_thesis: for A being non empty closed_interval Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds
( f1 - f2 is_integrable_on A & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds
( f1 - f2 is_integrable_on A & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
let f1, f2 be PartFunc of REAL, the carrier of X; ::_thesis: ( f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 implies ( f1 - f2 is_integrable_on A & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) )
assume that
A1: ( f1 is_integrable_on A & f2 is_integrable_on A ) and
A2: ( A c= dom f1 & A c= dom f2 ) ; ::_thesis: ( f1 - f2 is_integrable_on A & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
A3: f1 - f2 = f1 + (- f2) by VFUNCT_1:25;
A4: dom (- f2) = dom f2 by VFUNCT_1:def_5;
A5: - f2 = (- 1) (#) f2 by VFUNCT_1:23;
then A6: - f2 is_integrable_on A by A1, A2, Th13;
hence  f1 - f2 is_integrable_on A by A1, A2, A3, A4, Th14; ::_thesis: integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A))
thus  integral ((f1 - f2),A) = integral ((f1 + (- f2)),A) by VFUNCT_1:25
.= (integral (f1,A)) + (integral ((- f2),A)) by A1, A2, A4, A6, Th14
.= (integral (f1,A)) + ((- 1) * (integral (f2,A))) by A1, A2, A5, Th13
.= (integral (f1,A)) + (- (integral (f2,A))) by RLVECT_1:16
.= (integral (f1,A)) - (integral (f2,A)) by RLVECT_1:def_11 ; ::_thesis: verum
end;

definition
let X be RealNormSpace;
let f be PartFunc of REAL, the carrier of X;
let a, b be real number ;
func integral (f,a,b) ->  Element of X equals :Def9: :: INTEGR18:def 9
 integral (f,['a,b']) if a <= b
otherwise  - (integral (f,['b,a']));
correctness
coherence
( ( a <= b implies integral (f,['a,b']) is Element of X ) & ( not a <= b implies - (integral (f,['b,a'])) is Element of X ) );
consistency
for b1 being Element of X holds verum;
;
end;

:: deftheorem Def9 defines integral INTEGR18:def_9_:_
 for X being RealNormSpace
for f being PartFunc of REAL, the carrier of X
for a, b being real number holds
( ( a <= b implies integral (f,a,b) = integral (f,['a,b']) ) & ( not a <= b implies integral (f,a,b) = - (integral (f,['b,a'])) ) );

theorem Th16: :: INTEGR18:16
for X being RealNormSpace
for f being PartFunc of REAL, the carrier of X
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
proof
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
for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
let f be PartFunc of REAL, the carrier of X; ::_thesis: for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
let A be non empty closed_interval Subset of REAL; ::_thesis: for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
let a, b be Real; ::_thesis: ( A = [.a,b.] implies integral (f,A) = integral (f,a,b) )
consider a1, b1 being Real such that
A1: a1 <= b1 and
A2: A = [.a1,b1.] by MEASURE5:14;
assume  A = [.a,b.] ; ::_thesis: integral (f,A) = integral (f,a,b)
then A3: ( a1 = a & b1 = b ) by A2, INTEGRA1:5;
then  integral (f,a,b) = integral (f,['a,b']) by A1, Def9;
hence  integral (f,A) = integral (f,a,b) by A1, A2, A3, INTEGRA5:def_3; ::_thesis: verum
end;

theorem Th17: :: INTEGR18:17
for X being RealNormSpace
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 )
proof
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 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
A4: len (S . i) = len (S . i) ;
now__::_thesis:_for_k_being_Element_of_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 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 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 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 Def4
.= 0. X by A3 ; ::_thesis: verum
end;
A10: 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 A11: 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 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 by Def5;
hence  f is_integrable_on A by Def7; ::_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
end;

theorem :: INTEGR18:18
for X being RealNormSpace
for f being PartFunc of REAL, the carrier of X
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.b,a.] & A c= dom f holds
- (integral (f,A)) = integral (f,a,b)
proof
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
for a, b being Real st A = [.b,a.] & A c= dom f holds
- (integral (f,A)) = integral (f,a,b)
let f be PartFunc of REAL, the carrier of X; ::_thesis: for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.b,a.] & A c= dom f holds
- (integral (f,A)) = integral (f,a,b)
let A be non empty closed_interval Subset of REAL; ::_thesis: for a, b being Real st A = [.b,a.] & A c= dom f holds
- (integral (f,A)) = integral (f,a,b)
let a, b be Real; ::_thesis: ( A = [.b,a.] & A c= dom f implies - (integral (f,A)) = integral (f,a,b) )
consider a1, b1 being Real such that
A1: a1 <= b1 and
A2: A = [.a1,b1.] by MEASURE5:14;
assume A3: ( A = [.b,a.] & A c= dom f ) ; ::_thesis: - (integral (f,A)) = integral (f,a,b)
then A4: ( a1 = b & b1 = a ) by A2, INTEGRA1:5;
now__::_thesis:_-_(integral_(f,A))_=_integral_(f,a,b)
percases ( b < a or b = a ) by A1, A4, XXREAL_0:1;
supposeA5: b < a ; ::_thesis: - (integral (f,A)) = integral (f,a,b)
then  integral (f,a,b) = - (integral (f,['b,a'])) by Def9;
hence  - (integral (f,A)) = integral (f,a,b) by A3, A5, INTEGRA5:def_3; ::_thesis: verum
end;
supposeA6: b = a ; ::_thesis: - (integral (f,A)) = integral (f,a,b)
 A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then  ( lower_bound A = b & upper_bound A = a ) by A3, INTEGRA1:5;
then A7: vol A = (upper_bound A) - (upper_bound A) by A6
.= 0 ;
A8: integral (f,a,b) = integral (f,A) by A3, A6, Th16;
A9: - (integral (f,a,b)) = - (integral (f,A)) by A3, A6, Th16;
 integral (f,a,b) = 0. X by A7, A3, Th17, A8;
hence  - (integral (f,A)) = integral (f,a,b) by A9, RLVECT_1:12; ::_thesis: verum
end;
end;
end;
hence  - (integral (f,A)) = integral (f,a,b) ; ::_thesis: verum
end;