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;

hence integral h = r * (integral f) by Def6, A3; :: thesis: verum

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) )

hence
h is integrable
; :: thesis: integral h = r * (integral f)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 S_{1}[ 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 S_{1}[k,p]

A11: for x being Element of NAT holds S_{1}[x,F . x]
from FUNCT_2:sch 3(A5);

defpred S_{2}[ 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 S_{2}[k,y]

A22: for x being Element of NAT holds S_{2}[x,Sf . x]
from FUNCT_2:sch 3(A12);

A23: middle_sum (f,Sf) is convergent by A1, A4;

A24: r * (middle_sum (f,Sf)) = middle_sum (h,S)

.= 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, A39; :: thesis: verum

end;( 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 S

( 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 S

proof

consider F being sequence of (REAL *) such that
let k be Element of NAT ; :: thesis: ex p being Element of REAL * st S_{1}[k,p]

defpred S_{2}[ 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 S_{2}[i,x]

A10: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds

S_{2}[i,p . i] ) )
from FINSEQ_1:sch 5(A7);

take p ; :: thesis: ( p is Element of REAL * & S_{1}[k,p] )

len p = len (T . k) by A10, FINSEQ_1:def 3;

hence ( p is Element of REAL * & S_{1}[k,p] )
by A10, A6, FINSEQ_1:def 11; :: thesis: verum

end;defpred S

( 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 S

proof

consider p being FinSequence of REAL such that
let i be Nat; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S_{2}[i,x] )

assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S_{2}[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 object 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: S_{2}[i,x]

thus S_{2}[i,x]
by A8, A9; :: thesis: verum

end;assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S

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 object 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: S

thus S

A10: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds

S

take p ; :: thesis: ( p is Element of REAL * & S

len p = len (T . k) by A10, FINSEQ_1:def 3;

hence ( p is Element of REAL * & S

A11: for x being Element of NAT holds S

defpred S

( 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 S

proof

consider Sf being sequence of ( the carrier of X *) such that
let k be Element of NAT ; :: thesis: ex y being Element of the carrier of X * st S_{2}[k,y]

defpred S_{3}[ 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 S_{3}[i,x]

A19: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds

S_{3}[i,q . i] ) )
from FINSEQ_1:sch 5(A14);

A20: len q = len (T . k) by A19, FINSEQ_1:def 3;

q is Element of the carrier of X * by FINSEQ_1:def 11;

hence ex y being Element of the carrier of X * st S_{2}[k,y]
by A13, A19; :: thesis: verum

end;defpred S

( (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 S

proof

consider q being FinSequence of the carrier of X such that
let i be Nat; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of the carrier of X st S_{3}[i,x] )

assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of the carrier of X st S_{3}[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 S_{3}[i,x]
by A16, A18; :: thesis: verum

end;assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of the carrier of X st S

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 S

A19: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds

S

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 )

then reconsider q = q as middle_volume of f,T . k by A20, Def1;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;( 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

q is Element of the carrier of X * by FINSEQ_1:def 11;

hence ex y being Element of the carrier of X * st S

A22: for x being Element of NAT holds S

now :: thesis: for k being Element of NAT holds Sf . k is middle_volume of f,T . k

then reconsider Sf = Sf as middle_volume_Sequence of f,T by Def3;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;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

A23: middle_sum (f,Sf) is convergent by A1, A4;

A24: r * (middle_sum (f,Sf)) = middle_sum (h,S)

proof

end;

A39: lim (r * (middle_sum (f,Sf))) =
r * (lim (middle_sum (f,Sf)))
by A23, NORMSP_1:28
now :: thesis: for n being Nat holds r * ((middle_sum (f,Sf)) . n) = (middle_sum (h,S)) . n

hence
r * (middle_sum (f,Sf)) = middle_sum (h,S)
by NORMSP_1:def 5; :: thesis: verumlet n be Nat; :: thesis: r * ((middle_sum (f,Sf)) . n) = (middle_sum (h,S)) . n

A25: n in NAT by ORDINAL1:def 12;

consider p being FinSequence of REAL such that

A26: ( 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, A25;

consider q being middle_volume of f,T . n such that

A27: ( 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, A25;

( len (Sf . n) = len (T . n) & len (S . n) = len (T . n) ) by Def1;

then A28: ( dom (Sf . n) = dom (T . n) & dom (S . n) = dom (T . n) ) by FINSEQ_3:29;

thus r * ((middle_sum (f,Sf)) . n) = r * (middle_sum (f,(Sf . n))) by Def4

.= r * (Sum (Sf . n))

.= Sum (S . n) by A38, Th3

.= middle_sum (h,(S . n))

.= (middle_sum (h,S)) . n by Def4 ; :: thesis: verum

end;A25: n in NAT by ORDINAL1:def 12;

consider p being FinSequence of REAL such that

A26: ( 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, A25;

consider q being middle_volume of f,T . n such that

A27: ( 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, A25;

( len (Sf . n) = len (T . n) & len (S . n) = len (T . n) ) by Def1;

then A28: ( 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)

then A38:
r (#) (Sf . n) = S . n
by A28, VFUNCT_1:def 4;(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 A29: 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

A30: ( t = (h | (divset ((T . n),i))) . ((F . n) . i) & (S . n) . i = (vol (divset ((T . n),i))) * t ) by A29, A28, A26;

consider z being Point of X such that

A31: ( (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 A27, A29, A28;

A32: (F . n) . i in divset ((T . n),i) by A31, RELAT_1:57;

(F . n) . i in A by A31;

then A33: (F . n) . i in dom h by FUNCT_2:def 1;

A34: (F . n) . i in dom f by A31, RELAT_1:57;

A35: f /. ((F . n) . i) = f . ((F . n) . i) by A34, PARTFUN1:def 6

.= z by A31, A32, FUNCT_1:49 ;

A36: t = (h | (divset ((T . n),i))) . ((F . n) . i) by A30

.= h . ((F . n) . i) by A32, FUNCT_1:49

.= h /. ((F . n) . i) by A33, PARTFUN1:def 6

.= r * (f /. ((F . n) . i)) by A33, A1, VFUNCT_1:def 4

.= r * z by A35 ;

A37: (vol (divset ((T . n),i))) * z = (Sf . n) . x by A31, A27

.= (Sf . n) /. x by A29, A28, PARTFUN1:def 6 ;

thus (S . n) /. x = (S . n) . x by A29, PARTFUN1:def 6

.= (vol (divset ((T . n),i))) * t by A30

.= (vol (divset ((T . n),i))) * (r * z) by A36

.= ((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 A37 ; :: thesis: verum

end;assume A29: 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

A30: ( t = (h | (divset ((T . n),i))) . ((F . n) . i) & (S . n) . i = (vol (divset ((T . n),i))) * t ) by A29, A28, A26;

consider z being Point of X such that

A31: ( (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 A27, A29, A28;

A32: (F . n) . i in divset ((T . n),i) by A31, RELAT_1:57;

(F . n) . i in A by A31;

then A33: (F . n) . i in dom h by FUNCT_2:def 1;

A34: (F . n) . i in dom f by A31, RELAT_1:57;

A35: f /. ((F . n) . i) = f . ((F . n) . i) by A34, PARTFUN1:def 6

.= z by A31, A32, FUNCT_1:49 ;

A36: t = (h | (divset ((T . n),i))) . ((F . n) . i) by A30

.= h . ((F . n) . i) by A32, FUNCT_1:49

.= h /. ((F . n) . i) by A33, PARTFUN1:def 6

.= r * (f /. ((F . n) . i)) by A33, A1, VFUNCT_1:def 4

.= r * z by A35 ;

A37: (vol (divset ((T . n),i))) * z = (Sf . n) . x by A31, A27

.= (Sf . n) /. x by A29, A28, PARTFUN1:def 6 ;

thus (S . n) /. x = (S . n) . x by A29, PARTFUN1:def 6

.= (vol (divset ((T . n),i))) * t by A30

.= (vol (divset ((T . n),i))) * (r * z) by A36

.= ((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 A37 ; :: thesis: verum

thus r * ((middle_sum (f,Sf)) . n) = r * (middle_sum (f,(Sf . n))) by Def4

.= r * (Sum (Sf . n))

.= Sum (S . n) by A38, Th3

.= middle_sum (h,(S . n))

.= (middle_sum (h,S)) . n by Def4 ; :: thesis: verum

.= 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, A39; :: thesis: verum

hence integral h = r * (integral f) by Def6, A3; :: thesis: verum