mode middle_volume of f,D -> ( ( ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( ) set ) ) means :: INTEGR18:def 1
( len it : ( ( Function-like V27(X : ( ( ) ( ) NORMSTR ) , REAL : ( ( ) ( non empty V52() ) set ) ) ) ( V13() V16(X : ( ( ) ( ) NORMSTR ) ) V17( REAL : ( ( ) ( non empty V52() ) set ) ) Function-like total V27(X : ( ( ) ( ) NORMSTR ) , REAL : ( ( ) ( non empty V52() ) set ) ) ) Element of K6(K7(X : ( ( ) ( ) NORMSTR ) ,REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) = len D : ( ( Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for i being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Nat) st i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Nat) in dom D : ( ( Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V13() ) Element of K6(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
ex c being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st
( c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in rng (f : ( ( Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) | (divset (D : ( ( Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Nat) )) : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V13() V16(A : ( ( ) ( ) Element of X : ( ( ) ( ) NORMSTR ) ) ) V17( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) Function-like ) Element of K6(K7(A : ( ( ) ( ) Element of X : ( ( ) ( ) NORMSTR ) ) , the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & it : ( ( Function-like V27(X : ( ( ) ( ) NORMSTR ) , REAL : ( ( ) ( non empty V52() ) set ) ) ) ( V13() V16(X : ( ( ) ( ) NORMSTR ) ) V17( REAL : ( ( ) ( non empty V52() ) set ) ) Function-like total V27(X : ( ( ) ( ) NORMSTR ) , REAL : ( ( ) ( non empty V52() ) set ) ) ) Element of K6(K7(X : ( ( ) ( ) NORMSTR ) ,REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Nat) : ( ( ) ( ) set ) = (vol (divset (D : ( ( Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Nat) )) : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V52() ) set ) ) * c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) ) ) );

func middle_sum (f,F) -> ( ( ) ( ) Point of ( ( ) ( ) set ) ) equals :: INTEGR18:def 2
Sum F : ( ( Function-like V27(X : ( ( ) ( ) NORMSTR ) , REAL : ( ( ) ( non empty V52() ) set ) ) ) ( V13() V16(X : ( ( ) ( ) NORMSTR ) ) V17( REAL : ( ( ) ( non empty V52() ) set ) ) Function-like total V27(X : ( ( ) ( ) NORMSTR ) , REAL : ( ( ) ( non empty V52() ) set ) ) ) Element of K6(K7(X : ( ( ) ( ) NORMSTR ) ,REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) ;

mode middle_volume_Sequence of f,T -> ( ( Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) )) ) ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) )) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) )) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) )) ) means :: INTEGR18:def 3
for k being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) holds it : ( ( Function-like V27(X : ( ( ) ( ) NORMSTR ) , REAL : ( ( ) ( non empty V52() ) set ) ) ) ( V13() V16(X : ( ( ) ( ) NORMSTR ) ) V17( REAL : ( ( ) ( non empty V52() ) set ) ) Function-like total V27(X : ( ( ) ( ) NORMSTR ) , REAL : ( ( ) ( non empty V52() ) set ) ) ) Element of K6(K7(X : ( ( ) ( ) NORMSTR ) ,REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V52() FinSequence-like FinSubsequence-like ) Element of the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) )) ) is ( ( ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) Function-like V52() FinSequence-like FinSubsequence-like ) middle_volume of f : ( ( Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,T : ( ( Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( non empty V52() ) set ) ) Function-like V37() V52() FinSequence-like FinSubsequence-like ) Division of A : ( ( ) ( ) Element of X : ( ( ) ( ) NORMSTR ) ) ) ) ;

func middle_sum (f,S) -> ( ( Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) ) sequence of ( ( ) ( ) set ) ) means :: INTEGR18:def 4
for i being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) holds it : ( ( Function-like ) ( V13() V16(f : ( ( Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V17(T : ( ( Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function-like ) Element of K6(K7(f : ( ( Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,T : ( ( Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) = middle_sum (f : ( ( Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,(S : ( ( Function-like V27(X : ( ( ) ( ) NORMSTR ) , REAL : ( ( ) ( non empty V52() ) set ) ) ) ( V13() V16(X : ( ( ) ( ) NORMSTR ) ) V17( REAL : ( ( ) ( non empty V52() ) set ) ) Function-like total V27(X : ( ( ) ( ) NORMSTR ) , REAL : ( ( ) ( non empty V52() ) set ) ) ) Element of K6(K7(X : ( ( ) ( ) NORMSTR ) ,REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) Function-like V52() FinSequence-like FinSubsequence-like ) middle_volume of f : ( ( Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,T : ( ( Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V52() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( non empty V52() ) set ) ) Function-like V37() V52() FinSequence-like FinSubsequence-like ) Division of A : ( ( ) ( ) Element of X : ( ( ) ( ) NORMSTR ) ) ) ) ) : ( ( ) ( ) Point of ( ( ) ( ) set ) ) ;

attr f is integrable means :: INTEGR18:def 5
ex I being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st
for T being ( ( Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , divs A : ( ( ) ( ) Element of X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( divs A : ( ( ) ( ) Element of X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , divs A : ( ( ) ( ) Element of X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) ) DivSequence of ( ( ) ( ) set ) )
for S being ( ( ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) )) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) )) ) ) middle_volume_Sequence of f : ( ( Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,T : ( ( Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) DivSequence of ( ( ) ( non empty ) set ) ) ) st delta T : ( ( Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) DivSequence of ( ( ) ( non empty ) set ) ) : ( ( Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V52() ) set ) ) ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( non empty V52() ) set ) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V52() ) set ) ) ) Element of K6(K7(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is convergent & lim (delta T : ( ( Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) DivSequence of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V52() ) set ) ) ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( non empty V52() ) set ) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V52() ) set ) ) ) Element of K6(K7(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V52() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( middle_sum (f : ( ( Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,S : ( ( ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) )) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) )) ) ) middle_volume_Sequence of f : ( ( Function-like V27(A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( non empty V13() V16(A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) ) V17( the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total V27(A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) Function of A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) DivSequence of ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) ) sequence of ( ( ) ( ) set ) ) is convergent & lim (middle_sum (f : ( ( Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) ( V13() V16(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) V17(X : ( ( ) ( ) NORMSTR ) ) Function-like V27(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,S : ( ( ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) )) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) * : ( ( ) ( non empty functional FinSequence-membered ) M12( the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) )) ) ) middle_volume_Sequence of f : ( ( Function-like V27(A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( non empty V13() V16(A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) ) V17( the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total V27(A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) Function of A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) , the carrier of X : ( ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) ( non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , divs A : ( ( non empty closed_interval ) ( non empty V65() V66() V142() closed_interval ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) DivSequence of ( ( ) ( non empty ) set ) ) ) )) : ( ( Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) ) V17( the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) Function-like total V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty V52() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) ) sequence of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) = I : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) );