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

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

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

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 * () ) )
assume A1: ( h = r (#) f & f is integrable ) ; :: thesis: ( h is integrable & integral h = r * () )
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 () = 0 holds
( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = r * () )
let T be DivSequence of A; :: thesis: for S being middle_volume_Sequence of h,T st delta T is convergent & lim () = 0 holds
( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = r * () )

let S be middle_volume_Sequence of h,T; :: thesis: ( delta T is convergent & lim () = 0 implies ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = r * () ) )
assume A4: ( delta T is convergent & lim () = 0 ) ; :: thesis: ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = r * () )
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 object such that
A9: ( x in dom (h | (divset ((T . k),i))) & c = (h | (divset ((T . k),i))) . x ) by ;
( x in dom h & x in divset ((T . k),i) ) by ;
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 take p ; :: thesis: ( p is Element of REAL * & S1[k,p] )
len p = len (T . k) by ;
hence ( p is Element of REAL * & S1[k,p] ) by ; :: thesis: verum
end;
consider F being sequence of () such that
A11: for x being Element of NAT holds S1[x,F . x] from 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 ;
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 ;
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 ;
(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 ; :: 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 A20: len q = len (T . k) by ;
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 ; :: thesis: verum
end;
then reconsider q = q as middle_volume of f,T . k by ;
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 ; :: thesis: verum
end;
consider Sf being sequence of ( the carrier of X *) such that
A22: for x being Element of NAT holds S2[x,Sf . x] from
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;
A23: middle_sum (f,Sf) is convergent by A1, A4;
A24: r * (middle_sum (f,Sf)) = middle_sum (h,S)
proof
now :: thesis: for n being Nat holds r * ((middle_sum (f,Sf)) . n) = (middle_sum (h,S)) . n
let 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 ;
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 ;
( 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)
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 ;
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 ;
A32: (F . n) . i in divset ((T . n),i) by ;
(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 ;
A35: f /. ((F . n) . i) = f . ((F . n) . i) by
.= z by ;
A36: t = (h | (divset ((T . n),i))) . ((F . n) . i) by A30
.= h . ((F . n) . i) by
.= h /. ((F . n) . i) by
.= r * (f /. ((F . n) . i)) by
.= r * z by A35 ;
A37: (vol (divset ((T . n),i))) * z = (Sf . n) . x by
.= (Sf . n) /. x by ;
thus (S . n) /. x = (S . n) . x by
.= (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;
then A38: r (#) (Sf . n) = S . n by ;
thus r * ((middle_sum (f,Sf)) . n) = r * (middle_sum (f,(Sf . n))) by Def4
.= r * (Sum (Sf . n))
.= Sum (S . n) by
.= 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;
A39: lim (r * (middle_sum (f,Sf))) = r * (lim (middle_sum (f,Sf))) by
.= r * () by Def6, A1, A4 ;
thus middle_sum (h,S) is convergent by ; :: thesis: lim (middle_sum (h,S)) = r * ()
thus lim (middle_sum (h,S)) = r * () by ; :: thesis: verum
end;
hence h is integrable ; :: thesis: integral h = r * ()
hence integral h = r * () by ; :: thesis: verum