:: INTEGR18 semantic presentation

REAL is non empty V52() set

K6(REAL) is set
COMPLEX is non empty V52() set
RAT is non empty V52() set
INT is non empty V52() 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

- 1 is V11() real ext-real non positive Element of REAL
f is non empty V65() V66() V142() closed_interval Element of K6(REAL)

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

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)

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)

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

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)

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

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)

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)

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)

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

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)

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

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

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

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)

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

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

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)

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

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)

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)

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

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)

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

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)

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

dom n is Element of K6(NAT)

K7(NAT,()) is set
K6(K7(NAT,())) is set
m is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) Element of K6(K7(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)

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

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

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

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)

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

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

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

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

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

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)

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

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)

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

dom n is Element of K6(NAT)

K7(NAT,()) is set
K6(K7(NAT,())) is set
m is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) Element of K6(K7(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)

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

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

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

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)

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

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)

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

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

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

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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)

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

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

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)

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

(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