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 epsilon-connected ordinal natural V11() real ext-real Element of NAT
(X,A,a,b,a1) . n is Element of the carrier of X
((X,A,a,b,a1) . n) - (0. X) is Element of the carrier of X
||.(((X,A,a,b,a1) . n) - (0. X)).|| is V11() real ext-real Element of REAL
(0. X) - (0. X) is Element of the carrier of X
||.((0. X) - (0. X)).|| is V11() real ext-real Element of REAL
(X,A,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
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)
(X,A,f) is Element of the carrier of X
- (X,A,f) is Element of the carrier of X
b is V11() real ext-real Element of REAL
a is V11() real ext-real Element of REAL
[.b,a.] 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)
['b,a'] is non empty V65() V66() V142() closed_interval Element of K6(REAL)
(X,['b,a'],f) is Element of the carrier of X
- (X,['b,a'],f) is Element of the carrier of X
lower_bound A is V11() real ext-real Element of REAL
upper_bound A is V11() real ext-real Element of REAL
[.(lower_bound A),(upper_bound A).] is Element of K6(REAL)
vol A is V11() real ext-real Element of REAL
(upper_bound A) - (lower_bound A) is V11() real ext-real Element of REAL
(upper_bound A) - (upper_bound A) is V11() real ext-real Element of REAL
- (X,f,a,b) is Element of the carrier of X
0. X is V83(X) Element of the carrier of X