:: INTEGR18 semantic presentation

REAL is non empty V52() set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K6(REAL)

K6(REAL) is set

COMPLEX is non empty V52() set

RAT is non empty V52() set

INT is non empty V52() set

omega is non empty epsilon-transitive epsilon-connected ordinal set

K6(omega) is set

K6(NAT) is set

K7(COMPLEX,COMPLEX) is set

K6(K7(COMPLEX,COMPLEX)) is set

K7(COMPLEX,REAL) is set

K6(K7(COMPLEX,REAL)) is set

K7(NAT,REAL) is set

K6(K7(NAT,REAL)) is set

ExtREAL is non empty set

{} is set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Function-like functional ext-real non positive non negative FinSequence-membered set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Function-like functional ext-real non positive non negative FinSequence-membered set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

- 1 is V11() real ext-real non positive Element of REAL

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

a is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

len a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

dom a is Element of K6(NAT)

A is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

Seg (len a) is V52() V69( len a) Element of K6(NAT)

b is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

divset (a,b) is non empty V65() V66() V142() closed_interval Element of K6(REAL)

A | (divset (a,b)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

rng (A | (divset (a,b))) is Element of K6( the carrier of X)

K6( the carrier of X) is set

vol (divset (a,b)) is V11() real ext-real Element of REAL

upper_bound (divset (a,b)) is V11() real ext-real Element of REAL

lower_bound (divset (a,b)) is V11() real ext-real Element of REAL

(upper_bound (divset (a,b))) - (lower_bound (divset (a,b))) is V11() real ext-real Element of REAL

dom A is Element of K6(f)

K6(f) is set

dom (A | (divset (a,b))) is Element of K6(f)

a1 is set

b1 is Element of the carrier of X

(vol (divset (a,b))) * b1 is Element of the carrier of X

b is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of X

dom b is Element of K6(NAT)

len b is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

A is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

a is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

b is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,A,a)

Sum b is Element of the carrier of X

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

divs f is non empty set

K7(NAT,(divs f)) is set

K6(K7(NAT,(divs f))) is set

the carrier of X * is non empty functional FinSequence-membered M12( the carrier of X)

K7(NAT,( the carrier of X *)) is set

K6(K7(NAT,( the carrier of X *))) is set

A is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

a is non empty V13() V16( NAT ) V17( divs f) Function-like total V27( NAT , divs f) Element of K6(K7(NAT,(divs f)))

b is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

a . b is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

the V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,A,a . b) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,A,a . b)

b1 is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like Element of the carrier of X *

b is non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) Element of K6(K7(NAT,( the carrier of X *)))

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

divs f is non empty set

K7(NAT,(divs f)) is set

K6(K7(NAT,(divs f))) is set

the carrier of X * is non empty functional FinSequence-membered M12( the carrier of X)

A is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

a is non empty V13() V16( NAT ) V17( divs f) Function-like total V27( NAT , divs f) Element of K6(K7(NAT,(divs f)))

b is non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) (X,f,A,a)

a1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

b . a1 is V13() V16( NAT ) Function-like V52() FinSequence-like FinSubsequence-like set

a . a1 is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

divs f is non empty set

K7(NAT,(divs f)) is set

K6(K7(NAT,(divs f))) is set

the carrier of X * is non empty functional FinSequence-membered M12( the carrier of X)

A is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

a is non empty V13() V16( NAT ) V17( divs f) Function-like total V27( NAT , divs f) Element of K6(K7(NAT,(divs f)))

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

b is non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) (X,f,A,a)

a1 is non empty V13() V16( NAT ) V17( the carrier of X) Function-like total V27( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

b1 is non empty V13() V16( NAT ) V17( the carrier of X) Function-like total V27( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

a1 . m is Element of the carrier of X

b1 . m is Element of the carrier of X

a . m is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

(X,f,A,a,b,m) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,A,a . m)

(X,f,A,(a . m),(X,f,A,a,b,m)) is Element of the carrier of X

Sum (X,f,A,a,b,m) is Element of the carrier of X

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

f is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of X

len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

A is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of X

len A is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

a is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of X

f + A is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of X

Sum a is Element of the carrier of X

Sum f is Element of the carrier of X

Sum A is Element of the carrier of X

(Sum f) + (Sum A) is Element of the carrier of X

dom f is Element of K6(NAT)

dom A is Element of K6(NAT)

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

f is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of X

len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

A is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of X

len A is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

a is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of X

f - A is V13() V16( NAT ) V17( the carrier of X) Function-like Element of K6(K7(NAT, the carrier of X))

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

Sum a is Element of the carrier of X

Sum f is Element of the carrier of X

Sum A is Element of the carrier of X

(Sum f) - (Sum A) is Element of the carrier of X

dom f is Element of K6(NAT)

dom A is Element of K6(NAT)

dom a is Element of K6(NAT)

(dom f) /\ (dom A) is Element of K6(NAT)

len a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

b is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

a . b is set

f /. b is Element of the carrier of X

A /. b is Element of the carrier of X

(f /. b) - (A /. b) is Element of the carrier of X

a /. b is Element of the carrier of X

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

A is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of X

f is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of X

Sum A is Element of the carrier of X

Sum f is Element of the carrier of X

a is V11() real ext-real Element of REAL

a (#) f is V13() V16( NAT ) V17( the carrier of X) Function-like Element of K6(K7(NAT, the carrier of X))

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

a * (Sum f) is Element of the carrier of X

dom A is Element of K6(NAT)

dom f is Element of K6(NAT)

len A is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

b is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

A . b is set

f /. b is Element of the carrier of X

a * (f /. b) is Element of the carrier of X

A /. b is Element of the carrier of X

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

A is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

divs f is non empty set

K7(NAT,(divs f)) is set

K6(K7(NAT,(divs f))) is set

the carrier of X * is non empty functional FinSequence-membered M12( the carrier of X)

a is Element of the carrier of X

b is Element of the carrier of X

a1 is non empty V13() V16( NAT ) V17( divs f) Function-like total V27( NAT , divs f) Element of K6(K7(NAT,(divs f)))

delta a1 is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) Element of K6(K7(NAT,REAL))

lim (delta a1) is V11() real ext-real Element of REAL

the non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) (X,f,A,a1) is non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) (X,f,A,a1)

(X,f,A,a1, the non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) (X,f,A,a1)) is non empty V13() V16( NAT ) V17( the carrier of X) Function-like total V27( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

lim (X,f,A,a1, the non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) (X,f,A,a1)) is Element of the carrier of X

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

A is V11() real ext-real Element of REAL

b is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

a is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

A (#) a is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

(X,f,b) is Element of the carrier of X

(X,f,a) is Element of the carrier of X

A * (X,f,a) is Element of the carrier of X

dom b is Element of K6(f)

K6(f) is set

dom a is Element of K6(f)

divs f is non empty set

K7(NAT,(divs f)) is set

K6(K7(NAT,(divs f))) is set

the carrier of X * is non empty functional FinSequence-membered M12( the carrier of X)

a1 is non empty V13() V16( NAT ) V17( divs f) Function-like total V27( NAT , divs f) Element of K6(K7(NAT,(divs f)))

delta a1 is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) Element of K6(K7(NAT,REAL))

lim (delta a1) is V11() real ext-real Element of REAL

b1 is non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) (X,f,b,a1)

REAL * is non empty functional FinSequence-membered M12( REAL )

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

a1 . m is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

len (a1 . m) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

dom (a1 . m) is Element of K6(NAT)

(X,f,b,a1,b1,m) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,b,a1 . m)

Seg (len (a1 . m)) is V52() V69( len (a1 . m)) Element of K6(NAT)

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

divset ((a1 . m),n) is non empty V65() V66() V142() closed_interval Element of K6(REAL)

b | (divset ((a1 . m),n)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (b | (divset ((a1 . m),n))) is Element of K6(f)

(X,f,b,a1,b1,m) . n is set

vol (divset ((a1 . m),n)) is V11() real ext-real Element of REAL

upper_bound (divset ((a1 . m),n)) is V11() real ext-real Element of REAL

lower_bound (divset ((a1 . m),n)) is V11() real ext-real Element of REAL

(upper_bound (divset ((a1 . m),n))) - (lower_bound (divset ((a1 . m),n))) is V11() real ext-real Element of REAL

rng (b | (divset ((a1 . m),n))) is Element of K6( the carrier of X)

K6( the carrier of X) is set

c is Element of the carrier of X

(vol (divset ((a1 . m),n))) * c is Element of the carrier of X

Sg is set

(b | (divset ((a1 . m),n))) . Sg is set

Sg is V11() real ext-real Element of REAL

(b | (divset ((a1 . m),n))) . Sg is set

n is V13() V16( NAT ) V17( REAL ) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of REAL

dom n is Element of K6(NAT)

len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

K7(NAT,(REAL *)) is set

K6(K7(NAT,(REAL *))) is set

m is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) Element of K6(K7(NAT,(REAL *)))

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

a1 . n is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

dom (a1 . n) is Element of K6(NAT)

m . n is V13() V16( NAT ) Function-like V52() FinSequence-like FinSubsequence-like Element of REAL *

len (a1 . n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

Seg (len (a1 . n)) is V52() V69( len (a1 . n)) Element of K6(NAT)

c is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

(m . n) . c is set

divset ((a1 . n),c) is non empty V65() V66() V142() closed_interval Element of K6(REAL)

a | (divset ((a1 . n),c)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (a | (divset ((a1 . n),c))) is Element of K6(f)

(a | (divset ((a1 . n),c))) . ((m . n) . c) is set

vol (divset ((a1 . n),c)) is V11() real ext-real Element of REAL

upper_bound (divset ((a1 . n),c)) is V11() real ext-real Element of REAL

lower_bound (divset ((a1 . n),c)) is V11() real ext-real Element of REAL

(upper_bound (divset ((a1 . n),c))) - (lower_bound (divset ((a1 . n),c))) is V11() real ext-real Element of REAL

(X,f,b,a1,b1,n) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,b,a1 . n)

Sg is V13() V16( NAT ) V17( REAL ) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of REAL

len Sg is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

Sg . c is set

b | (divset ((a1 . n),c)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (b | (divset ((a1 . n),c))) is Element of K6(f)

(a | (divset ((a1 . n),c))) . (Sg . c) is set

rng (a | (divset ((a1 . n),c))) is Element of K6( the carrier of X)

K6( the carrier of X) is set

Sg is Element of the carrier of X

(vol (divset ((a1 . n),c))) * Sg is Element of the carrier of X

c is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of X

dom c is Element of K6(NAT)

len c is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

Sg is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

(m . n) . Sg is set

divset ((a1 . n),Sg) is non empty V65() V66() V142() closed_interval Element of K6(REAL)

a | (divset ((a1 . n),Sg)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (a | (divset ((a1 . n),Sg))) is Element of K6(f)

(a | (divset ((a1 . n),Sg))) . ((m . n) . Sg) is set

c . Sg is set

vol (divset ((a1 . n),Sg)) is V11() real ext-real Element of REAL

upper_bound (divset ((a1 . n),Sg)) is V11() real ext-real Element of REAL

lower_bound (divset ((a1 . n),Sg)) is V11() real ext-real Element of REAL

(upper_bound (divset ((a1 . n),Sg))) - (lower_bound (divset ((a1 . n),Sg))) is V11() real ext-real Element of REAL

Sg is Element of the carrier of X

(vol (divset ((a1 . n),Sg))) * Sg is Element of the carrier of X

rng (a | (divset ((a1 . n),Sg))) is Element of K6( the carrier of X)

K6( the carrier of X) is set

Sg is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,a,a1 . n)

K7(NAT,( the carrier of X *)) is set

K6(K7(NAT,( the carrier of X *))) is set

n is non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) Element of K6(K7(NAT,( the carrier of X *)))

c is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

a1 . c is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

n . c is V13() V16( NAT ) Function-like V52() FinSequence-like FinSubsequence-like Element of the carrier of X *

dom (a1 . c) is Element of K6(NAT)

m . c is V13() V16( NAT ) Function-like V52() FinSequence-like FinSubsequence-like Element of REAL *

Sg is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,a,a1 . c)

c is non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) (X,f,a,a1)

(X,f,a,a1,c) is non empty V13() V16( NAT ) V17( the carrier of X) Function-like total V27( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

A * (X,f,a,a1,c) is non empty V13() V16( NAT ) V17( the carrier of X) Function-like total V27( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

(X,f,b,a1,b1) is non empty V13() V16( NAT ) V17( the carrier of X) Function-like total V27( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

Sg is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

m . Sg is V13() V16( NAT ) Function-like V52() FinSequence-like FinSubsequence-like Element of REAL *

a1 . Sg is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

len (a1 . Sg) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

dom (a1 . Sg) is Element of K6(NAT)

(X,f,b,a1,b1,Sg) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,b,a1 . Sg)

Sg is V13() V16( NAT ) V17( REAL ) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of REAL

len Sg is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

(X,f,a,a1,c,Sg) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,a,a1 . Sg)

n is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,a,a1 . Sg)

len (X,f,a,a1,c,Sg) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

len (X,f,b,a1,b1,Sg) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

dom (X,f,a,a1,c,Sg) is Element of K6(NAT)

dom (X,f,b,a1,b1,Sg) is Element of K6(NAT)

p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

q is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

divset ((a1 . Sg),q) is non empty V65() V66() V142() closed_interval Element of K6(REAL)

b | (divset ((a1 . Sg),q)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

(m . Sg) . q is set

(b | (divset ((a1 . Sg),q))) . ((m . Sg) . q) is set

(X,f,b,a1,b1,Sg) . q is set

vol (divset ((a1 . Sg),q)) is V11() real ext-real Element of REAL

upper_bound (divset ((a1 . Sg),q)) is V11() real ext-real Element of REAL

lower_bound (divset ((a1 . Sg),q)) is V11() real ext-real Element of REAL

(upper_bound (divset ((a1 . Sg),q))) - (lower_bound (divset ((a1 . Sg),q))) is V11() real ext-real Element of REAL

r is Element of the carrier of X

(vol (divset ((a1 . Sg),q))) * r is Element of the carrier of X

a | (divset ((a1 . Sg),q)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (a | (divset ((a1 . Sg),q))) is Element of K6(f)

(a | (divset ((a1 . Sg),q))) . ((m . Sg) . q) is set

n . q is set

i is Element of the carrier of X

(vol (divset ((a1 . Sg),q))) * i is Element of the carrier of X

a /. ((m . Sg) . q) is Element of the carrier of X

a . ((m . Sg) . q) is set

b . ((m . Sg) . q) is set

b /. ((m . Sg) . q) is Element of the carrier of X

A * (a /. ((m . Sg) . q)) is Element of the carrier of X

A * i is Element of the carrier of X

(X,f,a,a1,c,Sg) . p is set

(X,f,a,a1,c,Sg) /. p is Element of the carrier of X

(X,f,b,a1,b1,Sg) /. p is Element of the carrier of X

(X,f,b,a1,b1,Sg) . p is set

(vol (divset ((a1 . Sg),q))) * (A * i) is Element of the carrier of X

(vol (divset ((a1 . Sg),q))) * A is V11() real ext-real Element of REAL

((vol (divset ((a1 . Sg),q))) * A) * i is Element of the carrier of X

A * ((vol (divset ((a1 . Sg),q))) * i) is Element of the carrier of X

A * ((X,f,a,a1,c,Sg) /. p) is Element of the carrier of X

A (#) (X,f,a,a1,c,Sg) is V13() V16( NAT ) V17( the carrier of X) Function-like Element of K6(K7(NAT, the carrier of X))

(X,f,a,a1,c) . Sg is Element of the carrier of X

A * ((X,f,a,a1,c) . Sg) is Element of the carrier of X

(X,f,a,(a1 . Sg),(X,f,a,a1,c,Sg)) is Element of the carrier of X

Sum (X,f,a,a1,c,Sg) is Element of the carrier of X

A * (X,f,a,(a1 . Sg),(X,f,a,a1,c,Sg)) is Element of the carrier of X

A * (Sum (X,f,a,a1,c,Sg)) is Element of the carrier of X

Sum (X,f,b,a1,b1,Sg) is Element of the carrier of X

(X,f,b,(a1 . Sg),(X,f,b,a1,b1,Sg)) is Element of the carrier of X

(X,f,b,a1,b1) . Sg is Element of the carrier of X

lim (A * (X,f,a,a1,c)) is Element of the carrier of X

lim (X,f,a,a1,c) is Element of the carrier of X

A * (lim (X,f,a,a1,c)) is Element of the carrier of X

lim (X,f,b,a1,b1) is Element of the carrier of X

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

a is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

A is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

- A is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

(X,f,a) is Element of the carrier of X

(X,f,A) is Element of the carrier of X

- (X,f,A) is Element of the carrier of X

(- 1) (#) A is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

(- 1) * (X,f,A) is Element of the carrier of X

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

b is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

A is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

a is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

A + a is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

(X,f,b) is Element of the carrier of X

(X,f,A) is Element of the carrier of X

(X,f,a) is Element of the carrier of X

(X,f,A) + (X,f,a) is Element of the carrier of X

dom b is Element of K6(f)

K6(f) is set

dom A is Element of K6(f)

dom a is Element of K6(f)

divs f is non empty set

K7(NAT,(divs f)) is set

K6(K7(NAT,(divs f))) is set

the carrier of X * is non empty functional FinSequence-membered M12( the carrier of X)

a1 is non empty V13() V16( NAT ) V17( divs f) Function-like total V27( NAT , divs f) Element of K6(K7(NAT,(divs f)))

delta a1 is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) Element of K6(K7(NAT,REAL))

lim (delta a1) is V11() real ext-real Element of REAL

b1 is non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) (X,f,b,a1)

REAL * is non empty functional FinSequence-membered M12( REAL )

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

a1 . m is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

len (a1 . m) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

dom (a1 . m) is Element of K6(NAT)

(X,f,b,a1,b1,m) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,b,a1 . m)

Seg (len (a1 . m)) is V52() V69( len (a1 . m)) Element of K6(NAT)

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

divset ((a1 . m),n) is non empty V65() V66() V142() closed_interval Element of K6(REAL)

b | (divset ((a1 . m),n)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (b | (divset ((a1 . m),n))) is Element of K6(f)

(X,f,b,a1,b1,m) . n is set

vol (divset ((a1 . m),n)) is V11() real ext-real Element of REAL

upper_bound (divset ((a1 . m),n)) is V11() real ext-real Element of REAL

lower_bound (divset ((a1 . m),n)) is V11() real ext-real Element of REAL

(upper_bound (divset ((a1 . m),n))) - (lower_bound (divset ((a1 . m),n))) is V11() real ext-real Element of REAL

rng (b | (divset ((a1 . m),n))) is Element of K6( the carrier of X)

K6( the carrier of X) is set

c is Element of the carrier of X

(vol (divset ((a1 . m),n))) * c is Element of the carrier of X

Sg is set

(b | (divset ((a1 . m),n))) . Sg is set

Sg is V11() real ext-real Element of REAL

(b | (divset ((a1 . m),n))) . Sg is set

n is V13() V16( NAT ) V17( REAL ) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of REAL

dom n is Element of K6(NAT)

len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

K7(NAT,(REAL *)) is set

K6(K7(NAT,(REAL *))) is set

m is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) Element of K6(K7(NAT,(REAL *)))

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

a1 . n is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

dom (a1 . n) is Element of K6(NAT)

m . n is V13() V16( NAT ) Function-like V52() FinSequence-like FinSubsequence-like Element of REAL *

len (a1 . n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

Seg (len (a1 . n)) is V52() V69( len (a1 . n)) Element of K6(NAT)

c is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

(m . n) . c is set

divset ((a1 . n),c) is non empty V65() V66() V142() closed_interval Element of K6(REAL)

A | (divset ((a1 . n),c)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (A | (divset ((a1 . n),c))) is Element of K6(f)

(A | (divset ((a1 . n),c))) . ((m . n) . c) is set

vol (divset ((a1 . n),c)) is V11() real ext-real Element of REAL

upper_bound (divset ((a1 . n),c)) is V11() real ext-real Element of REAL

lower_bound (divset ((a1 . n),c)) is V11() real ext-real Element of REAL

(upper_bound (divset ((a1 . n),c))) - (lower_bound (divset ((a1 . n),c))) is V11() real ext-real Element of REAL

(X,f,b,a1,b1,n) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,b,a1 . n)

Sg is V13() V16( NAT ) V17( REAL ) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of REAL

len Sg is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

Sg . c is set

b | (divset ((a1 . n),c)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (b | (divset ((a1 . n),c))) is Element of K6(f)

(A | (divset ((a1 . n),c))) . (Sg . c) is set

rng (A | (divset ((a1 . n),c))) is Element of K6( the carrier of X)

K6( the carrier of X) is set

Sg is Element of the carrier of X

(vol (divset ((a1 . n),c))) * Sg is Element of the carrier of X

c is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of X

dom c is Element of K6(NAT)

len c is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

Sg is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

(m . n) . Sg is set

divset ((a1 . n),Sg) is non empty V65() V66() V142() closed_interval Element of K6(REAL)

A | (divset ((a1 . n),Sg)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (A | (divset ((a1 . n),Sg))) is Element of K6(f)

(A | (divset ((a1 . n),Sg))) . ((m . n) . Sg) is set

c . Sg is set

vol (divset ((a1 . n),Sg)) is V11() real ext-real Element of REAL

upper_bound (divset ((a1 . n),Sg)) is V11() real ext-real Element of REAL

lower_bound (divset ((a1 . n),Sg)) is V11() real ext-real Element of REAL

(upper_bound (divset ((a1 . n),Sg))) - (lower_bound (divset ((a1 . n),Sg))) is V11() real ext-real Element of REAL

Sg is Element of the carrier of X

(vol (divset ((a1 . n),Sg))) * Sg is Element of the carrier of X

rng (A | (divset ((a1 . n),Sg))) is Element of K6( the carrier of X)

K6( the carrier of X) is set

Sg is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,A,a1 . n)

K7(NAT,( the carrier of X *)) is set

K6(K7(NAT,( the carrier of X *))) is set

n is non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) Element of K6(K7(NAT,( the carrier of X *)))

c is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

a1 . c is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

n . c is V13() V16( NAT ) Function-like V52() FinSequence-like FinSubsequence-like Element of the carrier of X *

dom (a1 . c) is Element of K6(NAT)

m . c is V13() V16( NAT ) Function-like V52() FinSequence-like FinSubsequence-like Element of REAL *

Sg is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,A,a1 . c)

Sg is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

a1 . Sg is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

dom (a1 . Sg) is Element of K6(NAT)

m . Sg is V13() V16( NAT ) Function-like V52() FinSequence-like FinSubsequence-like Element of REAL *

len (a1 . Sg) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

Seg (len (a1 . Sg)) is V52() V69( len (a1 . Sg)) Element of K6(NAT)

Sg is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

(m . Sg) . Sg is set

divset ((a1 . Sg),Sg) is non empty V65() V66() V142() closed_interval Element of K6(REAL)

a | (divset ((a1 . Sg),Sg)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (a | (divset ((a1 . Sg),Sg))) is Element of K6(f)

(a | (divset ((a1 . Sg),Sg))) . ((m . Sg) . Sg) is set

vol (divset ((a1 . Sg),Sg)) is V11() real ext-real Element of REAL

upper_bound (divset ((a1 . Sg),Sg)) is V11() real ext-real Element of REAL

lower_bound (divset ((a1 . Sg),Sg)) is V11() real ext-real Element of REAL

(upper_bound (divset ((a1 . Sg),Sg))) - (lower_bound (divset ((a1 . Sg),Sg))) is V11() real ext-real Element of REAL

(X,f,b,a1,b1,Sg) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,b,a1 . Sg)

n is V13() V16( NAT ) V17( REAL ) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of REAL

len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

n . Sg is set

b | (divset ((a1 . Sg),Sg)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (b | (divset ((a1 . Sg),Sg))) is Element of K6(f)

(a | (divset ((a1 . Sg),Sg))) . (n . Sg) is set

rng (a | (divset ((a1 . Sg),Sg))) is Element of K6( the carrier of X)

K6( the carrier of X) is set

p is Element of the carrier of X

(vol (divset ((a1 . Sg),Sg))) * p is Element of the carrier of X

Sg is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of X

dom Sg is Element of K6(NAT)

len Sg is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

(m . Sg) . n is set

divset ((a1 . Sg),n) is non empty V65() V66() V142() closed_interval Element of K6(REAL)

a | (divset ((a1 . Sg),n)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (a | (divset ((a1 . Sg),n))) is Element of K6(f)

(a | (divset ((a1 . Sg),n))) . ((m . Sg) . n) is set

Sg . n is set

vol (divset ((a1 . Sg),n)) is V11() real ext-real Element of REAL

upper_bound (divset ((a1 . Sg),n)) is V11() real ext-real Element of REAL

lower_bound (divset ((a1 . Sg),n)) is V11() real ext-real Element of REAL

(upper_bound (divset ((a1 . Sg),n))) - (lower_bound (divset ((a1 . Sg),n))) is V11() real ext-real Element of REAL

p is Element of the carrier of X

(vol (divset ((a1 . Sg),n))) * p is Element of the carrier of X

rng (a | (divset ((a1 . Sg),n))) is Element of K6( the carrier of X)

K6( the carrier of X) is set

n is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,a,a1 . Sg)

Sg is non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) Element of K6(K7(NAT,( the carrier of X *)))

Sg is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

a1 . Sg is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

Sg . Sg is V13() V16( NAT ) Function-like V52() FinSequence-like FinSubsequence-like Element of the carrier of X *

dom (a1 . Sg) is Element of K6(NAT)

m . Sg is V13() V16( NAT ) Function-like V52() FinSequence-like FinSubsequence-like Element of REAL *

n is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,a,a1 . Sg)

c is non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) (X,f,A,a1)

(X,f,A,a1,c) is non empty V13() V16( NAT ) V17( the carrier of X) Function-like total V27( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

lim (X,f,A,a1,c) is Element of the carrier of X

Sg is non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) (X,f,a,a1)

(X,f,a,a1,Sg) is non empty V13() V16( NAT ) V17( the carrier of X) Function-like total V27( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

lim (X,f,a,a1,Sg) is Element of the carrier of X

(X,f,A,a1,c) + (X,f,a,a1,Sg) is non empty V13() V16( NAT ) V17( the carrier of X) Function-like total V27( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

(X,f,b,a1,b1) is non empty V13() V16( NAT ) V17( the carrier of X) Function-like total V27( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

m . n is V13() V16( NAT ) Function-like V52() FinSequence-like FinSubsequence-like Element of REAL *

a1 . n is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of f

len (a1 . n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

dom (a1 . n) is Element of K6(NAT)

(X,f,b,a1,b1,n) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,b,a1 . n)

p is V13() V16( NAT ) V17( REAL ) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of REAL

len p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

(X,f,A,a1,c,n) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,A,a1 . n)

q is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,A,a1 . n)

(X,f,a,a1,Sg,n) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,a,a1 . n)

r is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,f,a,a1 . n)

len (X,f,A,a1,c,n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

len (X,f,a,a1,Sg,n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

len (X,f,b,a1,b1,n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

dom (X,f,A,a1,c,n) is Element of K6(NAT)

dom (X,f,a,a1,Sg,n) is Element of K6(NAT)

dom (X,f,b,a1,b1,n) is Element of K6(NAT)

i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set

Seg (len (X,f,b,a1,b1,n)) is V52() V69( len (X,f,b,a1,b1,n)) Element of K6(NAT)

divset ((a1 . n),i) is non empty V65() V66() V142() closed_interval Element of K6(REAL)

b | (divset ((a1 . n),i)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

(m . n) . i is set

(b | (divset ((a1 . n),i))) . ((m . n) . i) is set

(X,f,b,a1,b1,n) . i is set

vol (divset ((a1 . n),i)) is V11() real ext-real Element of REAL

upper_bound (divset ((a1 . n),i)) is V11() real ext-real Element of REAL

lower_bound (divset ((a1 . n),i)) is V11() real ext-real Element of REAL

(upper_bound (divset ((a1 . n),i))) - (lower_bound (divset ((a1 . n),i))) is V11() real ext-real Element of REAL

t is Element of the carrier of X

(vol (divset ((a1 . n),i))) * t is Element of the carrier of X

A | (divset ((a1 . n),i)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (A | (divset ((a1 . n),i))) is Element of K6(f)

(A | (divset ((a1 . n),i))) . ((m . n) . i) is set

q . i is set

z is Element of the carrier of X

(vol (divset ((a1 . n),i))) * z is Element of the carrier of X

a | (divset ((a1 . n),i)) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (a | (divset ((a1 . n),i))) is Element of K6(f)

(a | (divset ((a1 . n),i))) . ((m . n) . i) is set

r . i is set

w is Element of the carrier of X

(vol (divset ((a1 . n),i))) * w is Element of the carrier of X

A /. ((m . n) . i) is Element of the carrier of X

A . ((m . n) . i) is set

a /. ((m . n) . i) is Element of the carrier of X

a . ((m . n) . i) is set

b . ((m . n) . i) is set

b /. ((m . n) . i) is Element of the carrier of X

(A /. ((m . n) . i)) + (a /. ((m . n) . i)) is Element of the carrier of X

z + w is Element of the carrier of X

(X,f,A,a1,c,n) . i is set

(X,f,A,a1,c,n) /. i is Element of the carrier of X

(X,f,a,a1,Sg,n) . i is set

(X,f,a,a1,Sg,n) /. i is Element of the carrier of X

(X,f,b,a1,b1,n) /. i is Element of the carrier of X

((vol (divset ((a1 . n),i))) * z) + ((vol (divset ((a1 . n),i))) * w) is Element of the carrier of X

((X,f,A,a1,c,n) /. i) + ((X,f,a,a1,Sg,n) /. i) is Element of the carrier of X

(X,f,A,a1,c,n) + (X,f,a,a1,Sg,n) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of X

(X,f,A,a1,c) . n is Element of the carrier of X

(X,f,a,a1,Sg) . n is Element of the carrier of X

((X,f,A,a1,c) . n) + ((X,f,a,a1,Sg) . n) is Element of the carrier of X

(X,f,A,(a1 . n),(X,f,A,a1,c,n)) is Element of the carrier of X

Sum (X,f,A,a1,c,n) is Element of the carrier of X

(X,f,A,(a1 . n),(X,f,A,a1,c,n)) + ((X,f,a,a1,Sg) . n) is Element of the carrier of X

(X,f,a,(a1 . n),(X,f,a,a1,Sg,n)) is Element of the carrier of X

Sum (X,f,a,a1,Sg,n) is Element of the carrier of X

(X,f,A,(a1 . n),(X,f,A,a1,c,n)) + (X,f,a,(a1 . n),(X,f,a,a1,Sg,n)) is Element of the carrier of X

(Sum (X,f,A,a1,c,n)) + (X,f,a,(a1 . n),(X,f,a,a1,Sg,n)) is Element of the carrier of X

(Sum (X,f,A,a1,c,n)) + (Sum (X,f,a,a1,Sg,n)) is Element of the carrier of X

Sum (X,f,b,a1,b1,n) is Element of the carrier of X

(X,f,b,(a1 . n),(X,f,b,a1,b1,n)) is Element of the carrier of X

(X,f,b,a1,b1) . n is Element of the carrier of X

lim (X,f,b,a1,b1) is Element of the carrier of X

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

b is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

A is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

a is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

A - a is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

(X,f,b) is Element of the carrier of X

(X,f,A) is Element of the carrier of X

(X,f,a) is Element of the carrier of X

(X,f,A) - (X,f,a) is Element of the carrier of X

- a is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

A + (- a) is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

dom (- a) is Element of K6(f)

K6(f) is set

dom a is Element of K6(f)

a1 is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

(X,f,a1) is Element of the carrier of X

(X,f,A) + (X,f,a1) is Element of the carrier of X

- (X,f,a) is Element of the carrier of X

(X,f,A) + (- (X,f,a)) is Element of the carrier of X

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(REAL, the carrier of X) is set

K6(K7(REAL, the carrier of X)) is set

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(REAL, the carrier of X) is set

K6(K7(REAL, the carrier of X)) is set

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

A is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

dom A is Element of K6(REAL)

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

A | f is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

dom (A | f) is Element of K6(REAL)

rng (A | f) is Element of K6( the carrier of X)

K6( the carrier of X) is set

a is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

(X,f,a) is Element of the carrier of X

b1 is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

b is Element of the carrier of X

(X,f,b1) is Element of the carrier of X

m is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

a1 is Element of the carrier of X

(X,f,m) is Element of the carrier of X

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(REAL, the carrier of X) is set

K6(K7(REAL, the carrier of X)) is set

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

A is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

A | f is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

a is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

b is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(REAL, the carrier of X) is set

K6(K7(REAL, the carrier of X)) is set

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

A is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

dom A is Element of K6(REAL)

A | f is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

a is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

(X,f,A) is Element of the carrier of X

(X,f,a) is Element of the carrier of X

X is non empty set

f is non empty set

A is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of A is non empty set

K7(X, the carrier of A) is set

K6(K7(X, the carrier of A)) is set

K7(f, the carrier of A) is set

K6(K7(f, the carrier of A)) is set

a is V13() V16(X) V17( the carrier of A) Function-like Element of K6(K7(X, the carrier of A))

b is V13() V16(X) V17( the carrier of A) Function-like Element of K6(K7(X, the carrier of A))

a + b is V13() V16(X) V17( the carrier of A) Function-like Element of K6(K7(X, the carrier of A))

a1 is V13() V16(f) V17( the carrier of A) Function-like Element of K6(K7(f, the carrier of A))

b1 is V13() V16(f) V17( the carrier of A) Function-like Element of K6(K7(f, the carrier of A))

a1 + b1 is V13() V16(f) V17( the carrier of A) Function-like Element of K6(K7(f, the carrier of A))

dom (a + b) is Element of K6(X)

K6(X) is set

dom a is Element of K6(X)

dom b is Element of K6(X)

(dom a) /\ (dom b) is Element of K6(X)

dom a1 is Element of K6(f)

K6(f) is set

dom b1 is Element of K6(f)

(dom a1) /\ (dom b1) is Element of K6(f)

m is Element of f

(a + b) /. m is Element of the carrier of A

a1 /. m is Element of the carrier of A

b1 /. m is Element of the carrier of A

(a1 /. m) + (b1 /. m) is Element of the carrier of A

X is non empty set

f is non empty set

A is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of A is non empty set

K7(X, the carrier of A) is set

K6(K7(X, the carrier of A)) is set

K7(f, the carrier of A) is set

K6(K7(f, the carrier of A)) is set

a is V13() V16(X) V17( the carrier of A) Function-like Element of K6(K7(X, the carrier of A))

b is V13() V16(X) V17( the carrier of A) Function-like Element of K6(K7(X, the carrier of A))

a - b is V13() V16(X) V17( the carrier of A) Function-like Element of K6(K7(X, the carrier of A))

a1 is V13() V16(f) V17( the carrier of A) Function-like Element of K6(K7(f, the carrier of A))

b1 is V13() V16(f) V17( the carrier of A) Function-like Element of K6(K7(f, the carrier of A))

a1 - b1 is V13() V16(f) V17( the carrier of A) Function-like Element of K6(K7(f, the carrier of A))

dom (a - b) is Element of K6(X)

K6(X) is set

dom a is Element of K6(X)

dom b is Element of K6(X)

(dom a) /\ (dom b) is Element of K6(X)

dom a1 is Element of K6(f)

K6(f) is set

dom b1 is Element of K6(f)

(dom a1) /\ (dom b1) is Element of K6(f)

m is Element of f

(a - b) /. m is Element of the carrier of A

a1 /. m is Element of the carrier of A

b1 /. m is Element of the carrier of A

(a1 /. m) - (b1 /. m) is Element of the carrier of A

X is V11() real ext-real Element of REAL

f is non empty set

A is non empty set

a is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of a is non empty set

K7(f, the carrier of a) is set

K6(K7(f, the carrier of a)) is set

K7(A, the carrier of a) is set

K6(K7(A, the carrier of a)) is set

b is V13() V16(f) V17( the carrier of a) Function-like Element of K6(K7(f, the carrier of a))

X (#) b is V13() V16(f) V17( the carrier of a) Function-like Element of K6(K7(f, the carrier of a))

a1 is V13() V16(A) V17( the carrier of a) Function-like Element of K6(K7(A, the carrier of a))

X (#) a1 is V13() V16(A) V17( the carrier of a) Function-like Element of K6(K7(A, the carrier of a))

dom (X (#) b) is Element of K6(f)

K6(f) is set

dom b is Element of K6(f)

dom a1 is Element of K6(A)

K6(A) is set

b1 is Element of A

(X (#) b) /. b1 is Element of the carrier of a

a1 /. b1 is Element of the carrier of a

X * (a1 /. b1) is Element of the carrier of a

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(REAL, the carrier of X) is set

K6(K7(REAL, the carrier of X)) is set

f is V11() real ext-real Element of REAL

A is non empty V65() V66() V142() closed_interval Element of K6(REAL)

a is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

dom a is Element of K6(REAL)

f (#) a is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

(X,A,(f (#) a)) is Element of the carrier of X

(X,A,a) is Element of the carrier of X

f * (X,A,a) is Element of the carrier of X

dom (f (#) a) is Element of K6(REAL)

K7(A, the carrier of X) is set

K6(K7(A, the carrier of X)) is set

a | A is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

b is non empty V13() V16(A) V17( the carrier of X) Function-like total V27(A, the carrier of X) Element of K6(K7(A, the carrier of X))

(f (#) a) | A is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

f (#) (a | A) is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

f (#) b is V13() V16(A) V17( the carrier of X) Function-like Element of K6(K7(A, the carrier of X))

a1 is non empty V13() V16(A) V17( the carrier of X) Function-like total V27(A, the carrier of X) Element of K6(K7(A, the carrier of X))

(X,A,a1) is Element of the carrier of X

(X,A,b) is Element of the carrier of X

f * (X,A,b) is Element of the carrier of X

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(REAL, the carrier of X) is set

K6(K7(REAL, the carrier of X)) is set

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

A is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

a is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

dom A is Element of K6(REAL)

dom a is Element of K6(REAL)

A + a is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

(X,f,(A + a)) is Element of the carrier of X

(X,f,A) is Element of the carrier of X

(X,f,a) is Element of the carrier of X

(X,f,A) + (X,f,a) is Element of the carrier of X

(dom A) /\ (dom a) is Element of K6(REAL)

dom (A + a) is Element of K6(REAL)

K7(f, the carrier of X) is set

K6(K7(f, the carrier of X)) is set

A | f is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

b is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

a | f is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

a1 is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

(A + a) | f is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

(A | f) + (a | f) is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

b + a1 is V13() V16(f) V17( the carrier of X) Function-like Element of K6(K7(f, the carrier of X))

b1 is non empty V13() V16(f) V17( the carrier of X) Function-like total V27(f, the carrier of X) Element of K6(K7(f, the carrier of X))

(X,f,b1) is Element of the carrier of X

(X,f,b) is Element of the carrier of X

(X,f,a1) is Element of the carrier of X

(X,f,b) + (X,f,a1) is Element of the carrier of X

(X,f,A) + (X,f,a1) is Element of the carrier of X

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(REAL, the carrier of X) is set

K6(K7(REAL, the carrier of X)) is set

f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

A is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

a is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

dom A is Element of K6(REAL)

dom a is Element of K6(REAL)

A - a is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

(X,f,(A - a)) is Element of the carrier of X

(X,f,A) is Element of the carrier of X

(X,f,a) is Element of the carrier of X

(X,f,A) - (X,f,a) is Element of the carrier of X

- a is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

A + (- a) is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

dom (- a) is Element of K6(REAL)

(- 1) (#) a is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

(X,f,(A + (- a))) is Element of the carrier of X

(X,f,(- a)) is Element of the carrier of X

(X,f,A) + (X,f,(- a)) is Element of the carrier of X

(- 1) * (X,f,a) is Element of the carrier of X

(X,f,A) + ((- 1) * (X,f,a)) is Element of the carrier of X

- (X,f,a) is Element of the carrier of X

(X,f,A) + (- (X,f,a)) is Element of the carrier of X

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(REAL, the carrier of X) is set

K6(K7(REAL, the carrier of X)) is set

A is V11() real ext-real set

a is V11() real ext-real set

['A,a'] is non empty V65() V66() V142() closed_interval Element of K6(REAL)

f is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

(X,['A,a'],f) is Element of the carrier of X

['a,A'] is non empty V65() V66() V142() closed_interval Element of K6(REAL)

(X,['a,A'],f) is Element of the carrier of X

- (X,['a,A'],f) is Element of the carrier of X

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(REAL, the carrier of X) is set

K6(K7(REAL, the carrier of X)) is set

f is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

A is non empty V65() V66() V142() closed_interval Element of K6(REAL)

(X,A,f) is Element of the carrier of X

a is V11() real ext-real Element of REAL

b is V11() real ext-real Element of REAL

[.a,b.] is Element of K6(REAL)

(X,f,a,b) is Element of the carrier of X

a1 is V11() real ext-real Element of REAL

b1 is V11() real ext-real Element of REAL

[.a1,b1.] is Element of K6(REAL)

['a,b'] is non empty V65() V66() V142() closed_interval Element of K6(REAL)

(X,['a,b'],f) is Element of the carrier of X

X is non empty V102() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V137() V138() RealNormSpace-like NORMSTR

the carrier of X is non empty set

K7(REAL, the carrier of X) is set

K6(K7(REAL, the carrier of X)) is set

0. X is V83(X) Element of the carrier of X

f is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

dom f is Element of K6(REAL)

A is non empty V65() V66() V142() closed_interval Element of K6(REAL)

vol A is V11() real ext-real Element of REAL

upper_bound A is V11() real ext-real Element of REAL

lower_bound A is V11() real ext-real Element of REAL

(upper_bound A) - (lower_bound A) is V11() real ext-real Element of REAL

(X,A,f) is Element of the carrier of X

rng f is Element of K6( the carrier of X)

K6( the carrier of X) is set

K7((dom f),(rng f)) is set

K6(K7((dom f),(rng f))) is set

K7((dom f), the carrier of X) is set

K6(K7((dom f), the carrier of X)) is set

K7(A, the carrier of X) is set

K6(K7(A, the carrier of X)) is set

f | A is V13() V16( REAL ) V17( the carrier of X) Function-like Element of K6(K7(REAL, the carrier of X))

divs A is non empty set

K7(NAT,(divs A)) is set

K6(K7(NAT,(divs A))) is set

the carrier of X * is non empty functional FinSequence-membered M12( the carrier of X)

a is non empty V13() V16(A) V17( the carrier of X) Function-like total V27(A, the carrier of X) Element of K6(K7(A, the carrier of X))

b is non empty V13() V16( NAT ) V17( divs A) Function-like total V27( NAT , divs A) Element of K6(K7(NAT,(divs A)))

delta b is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) Element of K6(K7(NAT,REAL))

lim (delta b) is V11() real ext-real Element of REAL

a1 is non empty V13() V16( NAT ) V17( the carrier of X * ) Function-like total V27( NAT , the carrier of X * ) (X,A,a,b)

(X,A,a,b,a1) is non empty V13() V16( NAT ) V17( the carrier of X) Function-like total V27( NAT , the carrier of X) Element of K6(K7(NAT, the carrier of X))

K7(NAT, the carrier of X) is set

K6(K7(NAT, the carrier of X)) is set

lim (X,A,a,b,a1) is Element of the carrier of X

b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

b . b1 is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of A

(X,A,a,b,a1,b1) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,A,a,b . b1)

(X,A,a,(b . b1),(X,A,a,b,a1,b1)) is Element of the carrier of X

Sum (X,A,a,b,a1,b1) is Element of the carrier of X

len (X,A,a,b,a1,b1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

dom (X,A,a,b,a1,b1) is Element of K6(NAT)

n is Element of the carrier of X

(X,A,a,b,a1,b1) . m is set

Seg (len (X,A,a,b,a1,b1)) is V52() V69( len (X,A,a,b,a1,b1)) Element of K6(NAT)

len (b . b1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

Seg (len (b . b1)) is V52() V69( len (b . b1)) Element of K6(NAT)

dom (b . b1) is Element of K6(NAT)

divset ((b . b1),m) is non empty V65() V66() V142() closed_interval Element of K6(REAL)

a | (divset ((b . b1),m)) is V13() V16(A) V17( the carrier of X) Function-like Element of K6(K7(A, the carrier of X))

rng (a | (divset ((b . b1),m))) is Element of K6( the carrier of X)

vol (divset ((b . b1),m)) is V11() real ext-real Element of REAL

upper_bound (divset ((b . b1),m)) is V11() real ext-real Element of REAL

lower_bound (divset ((b . b1),m)) is V11() real ext-real Element of REAL

(upper_bound (divset ((b . b1),m))) - (lower_bound (divset ((b . b1),m))) is V11() real ext-real Element of REAL

c is Element of the carrier of X

(vol (divset ((b . b1),m))) * c is Element of the carrier of X

- n is Element of the carrier of X

- (Sum (X,A,a,b,a1,b1)) is Element of the carrier of X

b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

(X,A,a,b,a1) . b1 is Element of the carrier of X

b . b1 is non empty V13() V16( NAT ) V17( REAL ) Function-like V37() V52() FinSequence-like FinSubsequence-like Division of A

(X,A,a,b,a1,b1) is V13() V16( NAT ) V17( the carrier of X) Function-like V52() FinSequence-like FinSubsequence-like (X,A,a,b . b1)

(X,A,a,(b . b1),(X,A,a,b,a1,b1)) is Element of the carrier of X

Sum (X,A,a,b,a1,b1) is Element of the carrier of X

b1 is V11() real ext-real Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT

n is epsilon-transitive <