:: INTEGR15 semantic presentation

REAL is non empty V32() V129() V130() V131() V135() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V32() V37() V38() V129() V130() V131() V132() V133() V134() V135() Element of K6(REAL)
K6(REAL) is V32() set
omega is non empty epsilon-transitive epsilon-connected ordinal V32() V37() V38() V129() V130() V131() V132() V133() V134() V135() set
K6(omega) is V32() set
K6(NAT) is V32() set
COMPLEX is non empty V32() V129() V135() set
RAT is non empty V32() V129() V130() V131() V132() V135() set
INT is non empty V32() V129() V130() V131() V132() V133() V135() set
K7(REAL,REAL) is V32() V119() V120() V121() set
K6(K7(REAL,REAL)) is V32() set
K316() is non empty V75() L8()
the carrier of K316() is set
K321() is non empty L8()
K322() is non empty V75() M13(K321())
K323() is non empty V75() V97() V157() M16(K321(),K322())
K325() is non empty V75() V97() V99() V101() L8()
K326() is non empty V75() V97() V157() M13(K325())
K7(COMPLEX,COMPLEX) is V32() V119() set
K6(K7(COMPLEX,COMPLEX)) is V32() set
K7(COMPLEX,REAL) is V32() V119() V120() V121() set
K6(K7(COMPLEX,REAL)) is V32() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
K7(1,1) is V17( RAT ) V17( INT ) V119() V120() V121() V122() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V17( RAT ) V17( INT ) V119() V120() V121() V122() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V119() V120() V121() set
K6(K7(K7(1,1),REAL)) is set
K7(K7(REAL,REAL),REAL) is V32() V119() V120() V121() set
K6(K7(K7(REAL,REAL),REAL)) is V32() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
K7(2,2) is V17( RAT ) V17( INT ) V119() V120() V121() V122() set
K7(K7(2,2),REAL) is V119() V120() V121() set
K6(K7(K7(2,2),REAL)) is set
K424(2) is non empty V73() V142() TopSpace-like V194() V195() V196() V197() V198() V199() V200() V206() L16()
the carrier of K424(2) is set
K7( the carrier of K424(2),REAL) is V119() V120() V121() set
K6(K7( the carrier of K424(2),REAL)) is set
K6( the carrier of K424(2)) is set
K7(NAT,REAL) is V32() V119() V120() V121() set
K6(K7(NAT,REAL)) is V32() set
REAL 1 is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7((REAL 1),(REAL 1)) is set
K6(K7((REAL 1),(REAL 1))) is set
REAL-NS 1 is non empty V52() V73() V194() V195() V196() V197() V198() V199() V200() V216() V217() strict V219() V225() L19()
the carrier of (REAL-NS 1) is set
K522((REAL-NS 1),(REAL-NS 1)) is non empty L19()
the carrier of K522((REAL-NS 1),(REAL-NS 1)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V32() V119() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is V32() set
K7(RAT,RAT) is V17( RAT ) V32() V119() V120() V121() set
K6(K7(RAT,RAT)) is V32() set
K7(K7(RAT,RAT),RAT) is V17( RAT ) V32() V119() V120() V121() set
K6(K7(K7(RAT,RAT),RAT)) is V32() set
K7(INT,INT) is V17( RAT ) V17( INT ) V32() V119() V120() V121() set
K6(K7(INT,INT)) is V32() set
K7(K7(INT,INT),INT) is V17( RAT ) V17( INT ) V32() V119() V120() V121() set
K6(K7(K7(INT,INT),INT)) is V32() set
K7(NAT,NAT) is V17( RAT ) V17( INT ) V32() V119() V120() V121() V122() set
K7(K7(NAT,NAT),NAT) is V17( RAT ) V17( INT ) V32() V119() V120() V121() V122() set
K6(K7(K7(NAT,NAT),NAT)) is V32() set
ExtREAL is non empty V130() set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real functional V32() V37() V39( {} ) FinSequence-membered ext-real non positive non negative V129() V130() V131() V132() V133() V134() V135() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real functional V32() V37() V39( {} ) FinSequence-membered ext-real non positive non negative V129() V130() V131() V132() V133() V134() V135() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered set
0 is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
K38(1) is V11() real ext-real non positive set
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Seg (len x) is non empty V32() V39( len x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (x,f) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,f)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,f))) is V129() V130() V131() Element of K6(REAL)
vol (divset (x,f)) is V11() real ext-real Element of REAL
upper_bound (divset (x,f)) is V11() real ext-real Element of REAL
lower_bound (divset (x,f)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,f))) - (lower_bound (divset (x,f))) is V11() real ext-real Element of REAL
dom Z is V129() V130() V131() Element of K6(n)
K6(n) is set
dom (Z | (divset (x,f))) is V129() V130() V131() Element of K6(n)
r is set
i is V11() real ext-real Element of REAL
i * (vol (divset (x,f))) is V11() real ext-real Element of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
dom f is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
len f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
lower_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
(lower_volume (Z,x)) . r is V11() real ext-real Element of REAL
f . r is V11() real ext-real Element of REAL
divset (x,r) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,r)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,r))) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (Z | (divset (x,r)))) is V11() real ext-real Element of REAL
vol (divset (x,r)) is V11() real ext-real Element of REAL
upper_bound (divset (x,r)) is V11() real ext-real Element of REAL
lower_bound (divset (x,r)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,r))) - (lower_bound (divset (x,r))) is V11() real ext-real Element of REAL
(lower_bound (rng (Z | (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
i is V11() real ext-real Element of REAL
i * (vol (divset (x,r))) is V11() real ext-real Element of REAL
rng Z is V129() V130() V131() Element of K6(REAL)
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
lower_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
f is V11() real ext-real Element of REAL
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
Seg (len x) is non empty V32() V39( len x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (x,r) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,r)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,r))) is V129() V130() V131() Element of K6(REAL)
vol (divset (x,r)) is V11() real ext-real Element of REAL
upper_bound (divset (x,r)) is V11() real ext-real Element of REAL
lower_bound (divset (x,r)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,r))) - (lower_bound (divset (x,r))) is V11() real ext-real Element of REAL
(lower_volume (Z,x)) . r is V11() real ext-real Element of REAL
((lower_volume (Z,x)) . r) + f is V11() real ext-real Element of REAL
dom Z is V129() V130() V131() Element of K6(n)
K6(n) is set
dom (Z | (divset (x,r))) is V129() V130() V131() Element of K6(n)
rng Z is V129() V130() V131() Element of K6(REAL)
i is set
k is V11() real ext-real Element of REAL
k * (vol (divset (x,r))) is V11() real ext-real Element of REAL
lower_bound (rng (Z | (divset (x,r)))) is V11() real ext-real Element of REAL
(lower_bound (rng (Z | (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
rfz is V11() real ext-real Element of REAL
lower_bound (rng (Z | (divset (x,r)))) is V11() real ext-real Element of REAL
f / (vol (divset (x,r))) is V11() real ext-real Element of REAL
(lower_bound (rng (Z | (divset (x,r))))) + (f / (vol (divset (x,r)))) is V11() real ext-real Element of REAL
rfz is V11() real ext-real set
(lower_bound (rng (Z | (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
rfz * (vol (divset (x,r))) is V11() real ext-real Element of REAL
((lower_bound (rng (Z | (divset (x,r))))) + (f / (vol (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
Si is V11() real ext-real Element of REAL
(f / (vol (divset (x,r)))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
((lower_volume (Z,x)) . r) + ((f / (vol (divset (x,r)))) * (vol (divset (x,r)))) is V11() real ext-real Element of REAL
r is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
dom r is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (x,i) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,i)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,i))) is V129() V130() V131() Element of K6(REAL)
r . i is V11() real ext-real Element of REAL
vol (divset (x,i)) is V11() real ext-real Element of REAL
upper_bound (divset (x,i)) is V11() real ext-real Element of REAL
lower_bound (divset (x,i)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,i))) - (lower_bound (divset (x,i))) is V11() real ext-real Element of REAL
(lower_volume (Z,x)) . i is V11() real ext-real Element of REAL
((lower_volume (Z,x)) . i) + f is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
k * (vol (divset (x,i))) is V11() real ext-real Element of REAL
rfz is V11() real ext-real Element of REAL
rfz * (vol (divset (x,i))) is V11() real ext-real Element of REAL
len r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (x,k) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,k)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,k))) is V129() V130() V131() Element of K6(REAL)
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
i . k is V11() real ext-real Element of REAL
vol (divset (x,k)) is V11() real ext-real Element of REAL
upper_bound (divset (x,k)) is V11() real ext-real Element of REAL
lower_bound (divset (x,k)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,k))) - (lower_bound (divset (x,k))) is V11() real ext-real Element of REAL
(lower_volume (Z,x)) . k is V11() real ext-real Element of REAL
((lower_volume (Z,x)) . k) + f is V11() real ext-real Element of REAL
rfz is V11() real ext-real Element of REAL
rfz * (vol (divset (x,k))) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
upper_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
f is V11() real ext-real Element of REAL
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
Seg (len x) is non empty V32() V39( len x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (x,r) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,r)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,r))) is V129() V130() V131() Element of K6(REAL)
vol (divset (x,r)) is V11() real ext-real Element of REAL
upper_bound (divset (x,r)) is V11() real ext-real Element of REAL
lower_bound (divset (x,r)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,r))) - (lower_bound (divset (x,r))) is V11() real ext-real Element of REAL
(upper_volume (Z,x)) . r is V11() real ext-real Element of REAL
((upper_volume (Z,x)) . r) - f is V11() real ext-real Element of REAL
dom Z is V129() V130() V131() Element of K6(n)
K6(n) is set
dom (Z | (divset (x,r))) is V129() V130() V131() Element of K6(n)
rng Z is V129() V130() V131() Element of K6(REAL)
i is set
k is V11() real ext-real Element of REAL
k * (vol (divset (x,r))) is V11() real ext-real Element of REAL
upper_bound (rng (Z | (divset (x,r)))) is V11() real ext-real Element of REAL
(upper_bound (rng (Z | (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
rfz is V11() real ext-real Element of REAL
upper_bound (rng (Z | (divset (x,r)))) is V11() real ext-real Element of REAL
f / (vol (divset (x,r))) is V11() real ext-real Element of REAL
(upper_bound (rng (Z | (divset (x,r))))) - (f / (vol (divset (x,r)))) is V11() real ext-real Element of REAL
rfz is V11() real ext-real set
(upper_bound (rng (Z | (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
rfz * (vol (divset (x,r))) is V11() real ext-real Element of REAL
Si is V11() real ext-real Element of REAL
((upper_bound (rng (Z | (divset (x,r))))) - (f / (vol (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
(f / (vol (divset (x,r)))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
((upper_volume (Z,x)) . r) - ((f / (vol (divset (x,r)))) * (vol (divset (x,r)))) is V11() real ext-real Element of REAL
r is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
dom r is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (x,i) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,i)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,i))) is V129() V130() V131() Element of K6(REAL)
r . i is V11() real ext-real Element of REAL
vol (divset (x,i)) is V11() real ext-real Element of REAL
upper_bound (divset (x,i)) is V11() real ext-real Element of REAL
lower_bound (divset (x,i)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,i))) - (lower_bound (divset (x,i))) is V11() real ext-real Element of REAL
(upper_volume (Z,x)) . i is V11() real ext-real Element of REAL
((upper_volume (Z,x)) . i) - f is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
k * (vol (divset (x,i))) is V11() real ext-real Element of REAL
rfz is V11() real ext-real Element of REAL
rfz * (vol (divset (x,i))) is V11() real ext-real Element of REAL
len r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (x,k) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,k)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,k))) is V129() V130() V131() Element of K6(REAL)
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
i . k is V11() real ext-real Element of REAL
vol (divset (x,k)) is V11() real ext-real Element of REAL
upper_bound (divset (x,k)) is V11() real ext-real Element of REAL
lower_bound (divset (x,k)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,k))) - (lower_bound (divset (x,k))) is V11() real ext-real Element of REAL
(upper_volume (Z,x)) . k is V11() real ext-real Element of REAL
((upper_volume (Z,x)) . k) - f is V11() real ext-real Element of REAL
rfz is V11() real ext-real Element of REAL
rfz * (vol (divset (x,k))) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
upper_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
f . r is V11() real ext-real Element of REAL
(upper_volume (Z,x)) . r is V11() real ext-real Element of REAL
divset (x,r) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,r)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,r))) is V129() V130() V131() Element of K6(REAL)
upper_bound (rng (Z | (divset (x,r)))) is V11() real ext-real Element of REAL
vol (divset (x,r)) is V11() real ext-real Element of REAL
upper_bound (divset (x,r)) is V11() real ext-real Element of REAL
lower_bound (divset (x,r)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,r))) - (lower_bound (divset (x,r))) is V11() real ext-real Element of REAL
(upper_bound (rng (Z | (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
i is V11() real ext-real Element of REAL
i * (vol (divset (x,r))) is V11() real ext-real Element of REAL
rng Z is V129() V130() V131() Element of K6(REAL)
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
f is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
Sum f is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
lower_sum (Z,x) is V11() real ext-real Element of REAL
lower_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (lower_volume (Z,x)) is V11() real ext-real Element of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
(n,Z,x,f) is V11() real ext-real Element of REAL
Sum f is V11() real ext-real Element of REAL
len (lower_volume (Z,x)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
(len x) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
len f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
Seg (len x) is non empty V32() V39( len x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
r . k is V11() real ext-real Element of REAL
i is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
i . k is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
upper_sum (Z,x) is V11() real ext-real Element of REAL
upper_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (upper_volume (Z,x)) is V11() real ext-real Element of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
(n,Z,x,f) is V11() real ext-real Element of REAL
Sum f is V11() real ext-real Element of REAL
len (upper_volume (Z,x)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
(len x) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
len f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
Seg (len x) is non empty V32() V39( len x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
i is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
i . k is V11() real ext-real Element of REAL
r is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
r . k is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
lower_sum (Z,x) is V11() real ext-real Element of REAL
lower_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (lower_volume (Z,x)) is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
(lower_sum (Z,x)) + f is V11() real ext-real Element of REAL
len (lower_volume (Z,x)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
(len x) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
f / (len x) is V11() real ext-real Element of REAL
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
k is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
(len x) |-> (f / (len x)) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
r is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
r + ((len x) |-> (f / (len x))) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
(n,Z,x,k) is V11() real ext-real Element of REAL
Sum k is V11() real ext-real Element of REAL
len k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
S is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
Seg (len x) is non empty V32() V39( len x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
xs is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
xs . S is V11() real ext-real Element of REAL
r . S is V11() real ext-real Element of REAL
(r . S) + (f / (len x)) is V11() real ext-real Element of REAL
((len x) |-> (f / (len x))) . S is V11() real ext-real Element of REAL
(r . S) + (((len x) |-> (f / (len x))) . S) is V11() real ext-real Element of REAL
Si is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
Si . S is V11() real ext-real Element of REAL
Sum xs is V11() real ext-real Element of REAL
Sum Si is V11() real ext-real Element of REAL
Sum r is V11() real ext-real Element of REAL
Sum ((len x) |-> (f / (len x))) is V11() real ext-real Element of REAL
(Sum r) + (Sum ((len x) |-> (f / (len x)))) is V11() real ext-real Element of REAL
(len x) * (f / (len x)) is V11() real ext-real Element of REAL
(Sum r) + ((len x) * (f / (len x))) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
upper_sum (Z,x) is V11() real ext-real Element of REAL
upper_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (upper_volume (Z,x)) is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
(upper_sum (Z,x)) - f is V11() real ext-real Element of REAL
len (upper_volume (Z,x)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
(len x) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
f / (len x) is V11() real ext-real Element of REAL
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
k is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
(len x) |-> (f / (len x)) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
r is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
r - ((len x) |-> (f / (len x))) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
(n,Z,x,k) is V11() real ext-real Element of REAL
Sum k is V11() real ext-real Element of REAL
len k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
S is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
Seg (len x) is non empty V32() V39( len x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r . S is V11() real ext-real Element of REAL
(r . S) - (f / (len x)) is V11() real ext-real Element of REAL
xs is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
xs . S is V11() real ext-real Element of REAL
((len x) |-> (f / (len x))) . S is V11() real ext-real Element of REAL
(r . S) - (((len x) |-> (f / (len x))) . S) is V11() real ext-real Element of REAL
Si is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
Si . S is V11() real ext-real Element of REAL
Sum Si is V11() real ext-real Element of REAL
Sum xs is V11() real ext-real Element of REAL
Sum r is V11() real ext-real Element of REAL
Sum ((len x) |-> (f / (len x))) is V11() real ext-real Element of REAL
(Sum r) - (Sum ((len x) |-> (f / (len x)))) is V11() real ext-real Element of REAL
(len x) * (f / (len x)) is V11() real ext-real Element of REAL
(Sum r) - ((len x) * (f / (len x))) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(NAT,(REAL *)) is V32() set
K6(K7(NAT,(REAL *))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
x . f is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
the V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . f) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . f)
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL *
f is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) Element of K6(K7(NAT,(REAL *)))
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
f is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,x)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
f . r is FinSequence-like set
x . r is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
f is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,x)
r is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
i is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
r . k is V11() real ext-real Element of REAL
i . k is V11() real ext-real Element of REAL
x . k is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
(n,Z,x,f,k) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . k)
(n,Z,(x . k),(n,Z,x,f,k)) is V11() real ext-real Element of REAL
Sum (n,Z,x,f,k) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
lower_sum (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
f is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,x)
(n,Z,x,f) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(lower_sum (Z,x)) . r is V11() real ext-real Element of REAL
(n,Z,x,f) . r is V11() real ext-real Element of REAL
x . r is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
(n,Z,x,f,r) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . r)
(n,Z,(x . r),(n,Z,x,f,r)) is V11() real ext-real Element of REAL
Sum (n,Z,x,f,r) is V11() real ext-real Element of REAL
lower_sum (Z,(x . r)) is V11() real ext-real Element of REAL
lower_volume (Z,(x . r)) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (lower_volume (Z,(x . r))) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
upper_sum (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
f is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,x)
(n,Z,x,f) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,x,f) . r is V11() real ext-real Element of REAL
(upper_sum (Z,x)) . r is V11() real ext-real Element of REAL
x . r is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
(n,Z,x,f,r) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . r)
(n,Z,(x . r),(n,Z,x,f,r)) is V11() real ext-real Element of REAL
Sum (n,Z,x,f,r) is V11() real ext-real Element of REAL
upper_sum (Z,(x . r)) is V11() real ext-real Element of REAL
upper_volume (Z,(x . r)) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (upper_volume (Z,(x . r))) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
lower_sum (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
f is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
x . r is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
lower_sum (Z,(x . r)) is V11() real ext-real Element of REAL
lower_volume (Z,(x . r)) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (lower_volume (Z,(x . r))) is V11() real ext-real Element of REAL
(lower_sum (Z,(x . r))) + f is V11() real ext-real Element of REAL
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . r)
(n,Z,(x . r),i) is V11() real ext-real Element of REAL
Sum i is V11() real ext-real Element of REAL
k is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL *
r is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) Element of K6(K7(NAT,(REAL *)))
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
x . k is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
i is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,x)
(n,Z,x,i,k) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . k)
lower_sum (Z,(x . k)) is V11() real ext-real Element of REAL
lower_volume (Z,(x . k)) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (lower_volume (Z,(x . k))) is V11() real ext-real Element of REAL
(lower_sum (Z,(x . k))) + f is V11() real ext-real Element of REAL
(n,Z,x,i) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
(n,Z,x,i) . k is V11() real ext-real Element of REAL
rfz is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . k)
(n,Z,(x . k),rfz) is V11() real ext-real Element of REAL
Sum rfz is V11() real ext-real Element of REAL
(lower_sum (Z,x)) . k is V11() real ext-real Element of REAL
((lower_sum (Z,x)) . k) + f is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
upper_sum (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
f is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
x . r is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
upper_sum (Z,(x . r)) is V11() real ext-real Element of REAL
upper_volume (Z,(x . r)) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (upper_volume (Z,(x . r))) is V11() real ext-real Element of REAL
(upper_sum (Z,(x . r))) - f is V11() real ext-real Element of REAL
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . r)
(n,Z,(x . r),i) is V11() real ext-real Element of REAL
Sum i is V11() real ext-real Element of REAL
k is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL *
r is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) Element of K6(K7(NAT,(REAL *)))
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
x . k is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
i is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,x)
(n,Z,x,i,k) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . k)
upper_sum (Z,(x . k)) is V11() real ext-real Element of REAL
upper_volume (Z,(x . k)) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (upper_volume (Z,(x . k))) is V11() real ext-real Element of REAL
(upper_sum (Z,(x . k))) - f is V11() real ext-real Element of REAL
(n,Z,x,i) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
(n,Z,x,i) . k is V11() real ext-real Element of REAL
rfz is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . k)
(n,Z,(x . k),rfz) is V11() real ext-real Element of REAL
Sum rfz is V11() real ext-real Element of REAL
(upper_sum (Z,x)) . k is V11() real ext-real Element of REAL
((upper_sum (Z,x)) . k) - f is V11() real ext-real Element of REAL
n is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim n is V11() real ext-real Element of REAL
lim x is V11() real ext-real Element of REAL
Z is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim Z is V11() real ext-real Element of REAL
f is V11() real ext-real set
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
max (r,i) is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
rfz is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
Si is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
Z . Si is V11() real ext-real Element of REAL
(Z . Si) - (lim n) is V11() real ext-real Element of REAL
abs ((Z . Si) - (lim n)) is V11() real ext-real Element of REAL
n . Si is V11() real ext-real Element of REAL
(n . Si) - (lim n) is V11() real ext-real Element of REAL
abs ((n . Si) - (lim n)) is V11() real ext-real Element of REAL
(lim n) - f is V11() real ext-real Element of REAL
(lim n) + f is V11() real ext-real Element of REAL
].((lim n) - f),((lim n) + f).[ is V129() V130() V131() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= (lim n) - f & not (lim n) + f <= b₁ ) } is set
xs is V11() real ext-real Element of REAL
x . Si is V11() real ext-real Element of REAL
(x . Si) - (lim x) is V11() real ext-real Element of REAL
abs ((x . Si) - (lim x)) is V11() real ext-real Element of REAL
(lim x) - f is V11() real ext-real Element of REAL
(lim x) + f is V11() real ext-real Element of REAL
].((lim x) - f),((lim x) + f).[ is V129() V130() V131() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= (lim x) - f & not (lim x) + f <= b₁ ) } is set
xs is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
integral Z is V11() real ext-real Element of REAL
upper_integral Z is V11() real ext-real Element of REAL
upper_sum_set Z is non empty V13() V16( divs n) V17( REAL ) Function-like total V27( divs n, REAL ) V119() V120() V121() Element of K6(K7((divs n),REAL))
K7((divs n),REAL) is V32() V119() V120() V121() set
K6(K7((divs n),REAL)) is V32() set
rng (upper_sum_set Z) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set Z)) is V11() real ext-real Element of REAL
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
delta x is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (delta x) is V11() real ext-real Element of REAL
f is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,x)
(n,Z,x,f) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (n,Z,x,f) is V11() real ext-real Element of REAL
dom Z is V129() V130() V131() Element of K6(n)
K6(n) is set
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
lower_sum (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(lower_sum (Z,x)) . r is V11() real ext-real Element of REAL
(n,Z,x,f) . r is V11() real ext-real Element of REAL
upper_sum (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,x,f) . r is V11() real ext-real Element of REAL
(upper_sum (Z,x)) . r is V11() real ext-real Element of REAL
lim (upper_sum (Z,x)) is V11() real ext-real Element of REAL
lim (lower_sum (Z,x)) is V11() real ext-real Element of REAL
(lim (upper_sum (Z,x))) - (lim (lower_sum (Z,x))) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
integral Z is V11() real ext-real Element of REAL
upper_integral Z is V11() real ext-real Element of REAL
upper_sum_set Z is non empty V13() V16( divs n) V17( REAL ) Function-like total V27( divs n, REAL ) V119() V120() V121() Element of K6(K7((divs n),REAL))
K7((divs n),REAL) is V32() V119() V120() V121() set
K6(K7((divs n),REAL)) is V32() set
rng (upper_sum_set Z) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set Z)) is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
f is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
delta f is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (delta f) is V11() real ext-real Element of REAL
r is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)
(n,Z,f,r) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (n,Z,f,r) is V11() real ext-real Element of REAL
dom Z is V129() V130() V131() Element of K6(n)
K6(n) is set
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
f is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
delta f is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (delta f) is V11() real ext-real Element of REAL
upper_sum (Z,f) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (upper_sum (Z,f)) is V11() real ext-real Element of REAL
the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f) is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)
(n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) . i is V11() real ext-real Element of REAL
(upper_sum (Z,f)) . i is V11() real ext-real Element of REAL
((n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) . i) - ((n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) . i) is V11() real ext-real Element of REAL
((upper_sum (Z,f)) . i) - ((n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) . i) is V11() real ext-real Element of REAL
(upper_sum (Z,f)) - (n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
((upper_sum (Z,f)) - (n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f))) . i is V11() real ext-real Element of REAL
i is V11() real ext-real set
k is V11() real ext-real Element of REAL
rfz is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)
(n,Z,f,rfz) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
Si is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(upper_sum (Z,f)) . Si is V11() real ext-real Element of REAL
((upper_sum (Z,f)) . Si) - k is V11() real ext-real Element of REAL
(n,Z,f,rfz) . Si is V11() real ext-real Element of REAL
(((upper_sum (Z,f)) . Si) - k) + k is V11() real ext-real Element of REAL
((n,Z,f,rfz) . Si) + k is V11() real ext-real Element of REAL
((upper_sum (Z,f)) . Si) - ((n,Z,f,rfz) . Si) is V11() real ext-real Element of REAL
(((n,Z,f,rfz) . Si) + k) - ((n,Z,f,rfz) . Si) is V11() real ext-real Element of REAL
(upper_sum (Z,f)) - (n,Z,f,rfz) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
((upper_sum (Z,f)) - (n,Z,f,rfz)) . Si is V11() real ext-real Element of REAL
lim ((upper_sum (Z,f)) - (n,Z,f,rfz)) is V11() real ext-real Element of REAL
lim (n,Z,f,rfz) is V11() real ext-real Element of REAL
(lim (upper_sum (Z,f))) - (lim (n,Z,f,rfz)) is V11() real ext-real Element of REAL
(lim (upper_sum (Z,f))) - x is V11() real ext-real Element of REAL
lim ((upper_sum (Z,f)) - (n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f))) is V11() real ext-real Element of REAL
lim (n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) is V11() real ext-real Element of REAL
(lim (upper_sum (Z,f))) - (lim (n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f))) is V11() real ext-real Element of REAL
f is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
delta f is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (delta f) is V11() real ext-real Element of REAL
lower_sum (Z,f) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (lower_sum (Z,f)) is V11() real ext-real Element of REAL
the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f) is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(lower_sum (Z,f)) . i is V11() real ext-real Element of REAL
(n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
(n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) . i is V11() real ext-real Element of REAL
((lower_sum (Z,f)) . i) - ((lower_sum (Z,f)) . i) is V11() real ext-real Element of REAL
((n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) . i) - ((lower_sum (Z,f)) . i) is V11() real ext-real Element of REAL
(n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) - (lower_sum (Z,f)) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
((n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) - (lower_sum (Z,f))) . i is V11() real ext-real Element of REAL
i is V11() real ext-real set
k is V11() real ext-real Element of REAL
rfz is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)
(n,Z,f,rfz) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
Si is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,f,rfz) . Si is V11() real ext-real Element of REAL
(lower_sum (Z,f)) . Si is V11() real ext-real Element of REAL
((lower_sum (Z,f)) . Si) + k is V11() real ext-real Element of REAL
((n,Z,f,rfz) . Si) - ((lower_sum (Z,f)) . Si) is V11() real ext-real Element of REAL
(((lower_sum (Z,f)) . Si) + k) - ((lower_sum (Z,f)) . Si) is V11() real ext-real Element of REAL
(n,Z,f,rfz) - (lower_sum (Z,f)) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
((n,Z,f,rfz) - (lower_sum (Z,f))) . Si is V11() real ext-real Element of REAL
lim ((n,Z,f,rfz) - (lower_sum (Z,f))) is V11() real ext-real Element of REAL
lim (n,Z,f,rfz) is V11() real ext-real Element of REAL
(lim (n,Z,f,rfz)) - (lim (lower_sum (Z,f))) is V11() real ext-real Element of REAL
x - (lim (lower_sum (Z,f))) is V11() real ext-real Element of REAL
lim ((n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) - (lower_sum (Z,f))) is V11() real ext-real Element of REAL
lim (n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) is V11() real ext-real Element of REAL
(lim (n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f))) - (lim (lower_sum (Z,f))) is V11() real ext-real Element of REAL
f is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
delta f is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (delta f) is V11() real ext-real Element of REAL
upper_sum (Z,f) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (upper_sum (Z,f)) is V11() real ext-real Element of REAL
lower_sum (Z,f) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (lower_sum (Z,f)) is V11() real ext-real Element of REAL
(lim (upper_sum (Z,f))) - (lim (lower_sum (Z,f))) is V11() real ext-real Element of REAL
(lim (upper_sum (Z,f))) - x is V11() real ext-real Element of REAL
x - x is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
Z is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
f is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of Z
len f is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
dom f is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
x is non empty V13() V16(Z) V17( REAL n) Function-like total V27(Z, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
Seg (len f) is non empty V32() V39( len f) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (f,r) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
x | (divset (f,r)) is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
rng (x | (divset (f,r))) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
K6((REAL n)) is set
vol (divset (f,r)) is V11() real ext-real Element of REAL
upper_bound (divset (f,r)) is V11() real ext-real Element of REAL
lower_bound (divset (f,r)) is V11() real ext-real Element of REAL
(upper_bound (divset (f,r))) - (lower_bound (divset (f,r))) is V11() real ext-real Element of REAL
dom x is V129() V130() V131() Element of K6(Z)
K6(Z) is set
dom (x | (divset (f,r))) is V129() V130() V131() Element of K6(Z)
i is set
k is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(vol (divset (f,r))) * k is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
r is V13() V16( NAT ) V17( REAL n) Function-like V32() FinSequence-like FinSubsequence-like complex-functions-valued ext-real-functions-valued real-functions-valued FinSequence of REAL n
dom r is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
len r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
Z is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
x is non empty V13() V16(Z) V17( REAL n) Function-like total V27(Z, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
f is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of Z
Seg n is V32() V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is V13() V16( NAT ) V17( REAL n) Function-like V32() FinSequence-like FinSubsequence-like complex-functions-valued ext-real-functions-valued real-functions-valued (n,Z,x,f)
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (k,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (k,n)) * r is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
rfz is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum rfz is V11() real ext-real Element of REAL
Si is V11() real ext-real Element of REAL
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
dom i is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (k,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (k,n)) * r is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
i . k is V11() real ext-real Element of REAL
rfz is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
i . rfz is V11() real ext-real Element of REAL
Si is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
xs is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
proj (Si,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
(proj (Si,n)) * r is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum xs is V11() real ext-real Element of REAL
len i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (k,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (k,n)) * r is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
i . k is V11() real ext-real Element of REAL
i is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
k is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
dom i is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
rfz is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
i . rfz is V11() real ext-real Element of REAL
k . rfz is V11() real ext-real Element of REAL
len i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
Si is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (Si,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (Si,n)) * r is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
i . Si is V11() real ext-real Element of REAL
k . Si is V11() real ext-real Element of REAL
xs is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum xs is V11() real ext-real Element of REAL
S is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum S is V11() real ext-real Element of REAL
len k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
len i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
dom k is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
Z is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
divs Z is non empty set
K7(NAT,(divs Z)) is V32() set
K6(K7(NAT,(divs Z))) is V32() set
(REAL n) * is non empty functional FinSequence-membered FinSequenceSet of REAL n
K7(NAT,((REAL n) *)) is V32() set
K6(K7(NAT,((REAL n) *))) is V32() set
x is non empty V13() V16(Z) V17( REAL n) Function-like total V27(Z, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
f is non empty V13() V16( NAT ) V17( divs Z) Function-like total V27( NAT , divs Z) Element of K6(K7(NAT,(divs Z)))
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
f . r is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of Z
the V13() V16( NAT ) V17( REAL n) Function-like V32() FinSequence-like FinSubsequence-like complex-functions-valued ext-real-functions-valued real-functions-valued (n,Z,x,f . r) is V13() V16( NAT ) V17( REAL n) Function-like V32() FinSequence-like FinSubsequence-like complex-functions-valued ext-real-functions-valued real-functions-valued (n,Z,x,f . r)
k is V13() V16( NAT ) V17( REAL n) Function-like V32() FinSequence-like FinSubsequence-like complex-functions-valued Element of (REAL n) *
r is non empty V13() V16( NAT ) V17((REAL n) * ) Function-like total V27( NAT ,(REAL n) * ) Element of K6(K7(NAT,((REAL n) *)))
Z is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
divs Z is non empty set
K7(NAT,(divs Z)) is V32() set
K6(K7(NAT,(divs Z))) is V32() set
(REAL n) * is non empty functional FinSequence-membered FinSequenceSet of REAL n
x is non empty V13() V16(Z) V17( REAL n) Function-like total V27(Z, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
f is non empty V13() V16( NAT ) V17( divs Z) Function-like total V27( NAT , divs Z) Element of K6(K7(NAT,(divs Z)))
r is non empty V13() V16( NAT ) V17((REAL n) * ) Function-like total V27( NAT ,(REAL n) * ) (n,Z,x,f)
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
r . i is FinSequence-like set
f . i is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of Z
Z is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
divs Z is non empty set
K7(NAT,(divs Z)) is V32() set
K6(K7(NAT,(divs Z))) is V32() set
(REAL n) * is non empty functional FinSequence-membered FinSequenceSet of REAL n
x is non empty V13() V16(Z) V17( REAL n) Function-like total V27(Z, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
f is non empty V13() V16( NAT ) V17( divs Z) Function-like total V27( NAT , divs Z) Element of K6(K7(NAT,(divs Z)))
REAL-NS n is non empty V73() V194() V195() V196() V197() V198() V199() V200() V216() V217() strict V219() V225() L19()
the carrier of (REAL-NS n) is set
K7(NAT, the carrier of (REAL-NS n)) is set
K6(K7(NAT, the carrier of (REAL-NS n))) is set
r is non empty V13() V16( NAT ) V17((REAL n) * ) Function-like total V27( NAT ,(REAL n) * ) (n,Z,x,f)
K7(NAT,(REAL n)) is V32() set
K6(K7(NAT,(REAL n))) is V32() set
i is non empty V13() V16( NAT ) V17( REAL n) Function-like total V27( NAT , REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(NAT,(REAL n)))
i is V13() V16( NAT ) V17( the carrier of (REAL-NS n)) Function-like V27( NAT , the carrier of (REAL-NS n)) Element of K6(K7(NAT, the carrier of (REAL-NS n)))
k is V13() V16( NAT ) V17( the carrier of (REAL-NS n)) Function-like V27( NAT , the carrier of (REAL-NS n)) Element of K6(K7(NAT, the carrier of (REAL-NS n)))
rfz is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
i . rfz is Element of the carrier of (REAL-NS n)
k . rfz is Element of the carrier of (REAL-NS n)
f . rfz is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of Z
(n,Z,x,f,r,rfz) is V13() V16( NAT ) V17( REAL n) Function-like V32() FinSequence-like FinSubsequence-like complex-functions-valued ext-real-functions-valued real-functions-valued (n,Z,x,f . rfz)
(n,Z,x,(f . rfz),(n,Z,x,f,r,rfz)) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
Z is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
x is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
f is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
x <++> f is V13() V16(Z /\ Z) V17( R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((Z /\ Z),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))))
Z /\ Z is set
DOMS (REAL n) is set
(DOMS (REAL n)) /\ (DOMS (REAL n)) is set
R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K7((Z /\ Z),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))) is set
K6(K7((Z /\ Z),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))))) is set
rng (x <++> f) is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))))
K6((R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))) is set
i is set
dom (x <++> f) is Element of K6((Z /\ Z))
K6((Z /\ Z)) is set
k is set
(x <++> f) . k is V13() Function-like V119() V120() V121() set
dom x is Element of K6(Z)
K6(Z) is set
dom f is Element of K6(Z)
(dom x) /\ (dom f) is Element of K6(Z)
x . k is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
x /. k is V39(n) FinSequence-like V119() V120() V121() Element of REAL n
f . k is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
f /. k is V39(n) FinSequence-like V119() V120() V121() Element of REAL n
(x /. k) + (f /. k) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
x <--> f is V13() V16(Z /\ Z) V17( R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((Z /\ Z),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))))
rng (x <--> f) is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))))
K6((R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))) is set
i is set
dom (x <--> f) is Element of K6((Z /\ Z))
K6((Z /\ Z)) is set
k is set
(x <--> f) . k is V13() Function-like V119() V120() V121() set
dom x is Element of K6(Z)
K6(Z) is set
dom f is Element of K6(Z)
(dom x) /\ (dom f) is Element of K6(Z)
x . k is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
x /. k is V39(n) FinSequence-like V119() V120() V121() Element of REAL n
f . k is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
f /. k is V39(n) FinSequence-like V119() V120() V121() Element of REAL n
(x /. k) - (f /. k) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
x is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(x,(REAL n)) is set
K6(K7(x,(REAL n))) is set
f is V13() V16(x) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(x,(REAL n)))
Z is V11() real ext-real set
f [#] Z is V13() V16(x) V17( R_PFuncs (DOMS (REAL n))) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(x,(R_PFuncs (DOMS (REAL n)))))
DOMS (REAL n) is set
R_PFuncs (DOMS (REAL n)) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K7(x,(R_PFuncs (DOMS (REAL n)))) is set
K6(K7(x,(R_PFuncs (DOMS (REAL n))))) is set
rng (f [#] Z) is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((R_PFuncs (DOMS (REAL n))))
K6((R_PFuncs (DOMS (REAL n)))) is set
i is set
dom (f [#] Z) is Element of K6(x)
K6(x) is set
k is set
(f [#] Z) . k is V13() Function-like V119() V120() V121() set
dom f is Element of K6(x)
f . k is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
f /. k is V39(n) FinSequence-like V119() V120() V121() Element of REAL n
Z * (f /. k) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
Z is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is V32() set
K6(K7(REAL,(REAL n))) is V32() set
x is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (f,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (f,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
r is V129() V130() V131() Element of K6(REAL)
x | r is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
(proj (f,n)) * (x | r) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
((proj (f,n)) * x) | r is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
dom (proj (f,n)) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
K6((REAL n)) is set
rng x is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
rng (x | r) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
i is set
dom (((proj (f,n)) * x) | r) is V129() V130() V131() Element of K6(REAL)
dom ((proj (f,n)) * x) is V129() V130() V131() Element of K6(REAL)
(dom ((proj (f,n)) * x)) /\ r is V129() V130() V131() Element of K6(REAL)
dom x is V129() V130() V131() Element of K6(REAL)
(dom x) /\ r is V129() V130() V131() Element of K6(REAL)
dom (x | r) is V129() V130() V131() Element of K6(REAL)
dom ((proj (f,n)) * (x | r)) is V129() V130() V131() Element of K6(REAL)
((proj (f,n)) * (x | r)) . i is V11() real ext-real Element of REAL
(x | r) . i is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
(proj (f,n)) . ((x | r) . i) is V11() real ext-real Element of REAL
x . i is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
(proj (f,n)) . (x . i) is V11() real ext-real Element of REAL
((proj (f,n)) * x) . i is V11() real ext-real Element of REAL
(((proj (f,n)) * x) | r) . i is V11() real ext-real Element of REAL
Z is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
Z is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
Seg n is V32() V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
x is non empty V13() V16(Z) V17( REAL n) Function-like total V27(Z, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * x is non empty V13() V16(Z) V17( REAL ) Function-like total V27(Z, REAL ) V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
integral ((proj (r,n)) * x) is V11() real ext-real Element of REAL
upper_integral ((proj (r,n)) * x) is V11() real ext-real Element of REAL
upper_sum_set ((proj (r,n)) * x) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
divs Z is non empty set
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set ((proj (r,n)) * x)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((proj (r,n)) * x))) is V11() real ext-real Element of REAL
i is V11() real ext-real Element of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
dom f is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
f . r is V11() real ext-real Element of REAL
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * x is non empty V13() V16(Z) V17( REAL ) Function-like total V27(Z, REAL ) V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
integral ((proj (r,n)) * x) is V11() real ext-real Element of REAL
upper_integral ((proj (r,n)) * x) is V11() real ext-real Element of REAL
upper_sum_set ((proj (r,n)) * x) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
divs Z is non empty set
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set ((proj (r,n)) * x)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((proj (r,n)) * x))) is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (i,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
(proj (i,n)) * x is non empty V13() V16(Z) V17( REAL ) Function-like total V27(Z, REAL ) V119() V120() V121() Element of K6(K7(Z,REAL))
integral ((proj (i,n)) * x) is V11() real ext-real Element of REAL
upper_integral ((proj (i,n)) * x) is V11() real ext-real Element of REAL
upper_sum_set ((proj (i,n)) * x) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
rng (upper_sum_set ((proj (i,n)) * x)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((proj (i,n)) * x))) is V11() real ext-real Element of REAL
len f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
f . r is V11() real ext-real Element of REAL
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * x is non empty V13() V16(Z) V17( REAL ) Function-like total V27(Z, REAL ) V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
integral ((proj (r,n)) * x) is V11() real ext-real Element of REAL
upper_integral ((proj (r,n)) * x) is V11() real ext-real Element of REAL
upper_sum_set ((proj (r,n)) * x) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
divs Z is non empty set
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set ((proj (r,n)) * x)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((proj (r,n)) * x))) is V11() real ext-real Element of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
dom f is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
dom r is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
f . k is V11() real ext-real Element of REAL
proj (k,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (k,n)) * x is non empty V13() V16(Z) V17( REAL ) Function-like total V27(Z, REAL ) V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
integral ((proj (k,n)) * x) is V11() real ext-real Element of REAL
upper_integral ((proj (k,n)) * x) is V11() real ext-real Element of REAL
upper_sum_set ((proj (k,n)) * x) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
divs Z is non empty set
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set ((proj (k,n)) * x)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((proj (k,n)) * x))) is V11() real ext-real Element of REAL
r . k is V11() real ext-real Element of REAL
f . i is V11() real ext-real Element of REAL
r . i is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
(REAL n) * is non empty functional FinSequence-membered FinSequenceSet of REAL n
REAL-NS n is non empty V73() V194() V195() V196() V197() V198() V199() V200() V216() V217() strict V219() V225() L19()
Z is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
divs Z is non empty set
K7(NAT,(divs Z)) is V32() set
K6(K7(NAT,(divs Z))) is V32() set
x is non empty V13() V16(Z) V17( REAL n) Function-like total V27(Z, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
(n,Z,x) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
f is non empty V13() V16( NAT ) V17( divs Z) Function-like total V27( NAT , divs Z) Element of K6(K7(NAT,(divs Z)))
delta f is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (delta f) is V11() real ext-real Element of REAL
r is non empty V13() V16( NAT ) V17((REAL n) * ) Function-like total V27( NAT ,(REAL n) * ) (n,Z,x,f)
(n,Z,x,f,r) is V13() V16( NAT ) V17( the carrier of (REAL-NS n)) Function-like V27( NAT , the carrier of (REAL-NS n)) Element of K6(K7(NAT, the carrier of (REAL-NS n)))
the carrier of (REAL-NS n) is set
K7(NAT, the carrier of (REAL-NS n)) is set
K6(K7(NAT, the carrier of (REAL-NS n))) is set
lim (n,Z,x,f,r) is Element of the carrier of (REAL-NS n)
K7(NAT,(REAL n)) is V32() set
K6(K7(NAT,(REAL n))) is V32() set
Seg n is V32() V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
rfz is non empty V13() V16( NAT ) V17( REAL n) Function-like total V27( NAT , REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(NAT,(REAL n)))
Si is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,x) . Si is V11() real ext-real Element of REAL
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
proj (Si,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (Si,n)) * x is non empty V13() V16(Z) V17( REAL ) Function-like total V27(Z, REAL ) V119() V120() V121() Element of K6(K7(Z,REAL))
S is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,x,f,r,S) is V13() V16( NAT ) V17( REAL n) Function-like V32() FinSequence-like FinSubsequence-like complex-functions-valued ext-real-functions-valued real-functions-valued (n,Z,x,f . S)
f . S is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of Z
(proj (Si,n)) * (n,Z,x,f,r,S) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
S is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) Element of K6(K7(NAT,(REAL *)))
S is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,x,f,r,S) is V13() V16( NAT ) V17( REAL n) Function-like V32() FinSequence-like FinSubsequence-like complex-functions-valued ext-real-functions-valued real-functions-valued (n,Z,x,f . S)
f . S is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of Z
(proj (Si,n)) * (n,Z,x,f,r,S) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
dom ((proj (Si,n)) * (n,Z,x,f,r,S)) is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
len (n,Z,x,f,r,S) is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
Seg (len (n,Z,x,f,r,S)) is V32() V39( len (n,Z,x,f,r,S)) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
rng ((proj (Si,n)) * (n,Z,x,f,r,S)) is V129() V130() V131() Element of K6(REAL)
dom (proj (Si,n)) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
K6((REAL n)) is set
rng (n,Z,x,f,r,S) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
dom (n,Z,x,f,r,S) is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
xs is non empty V13() V16(Z) V17( REAL ) Function-like total V27(Z, REAL ) V119() V120() V121() Element of K6(K7(Z,REAL))
S is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
S . S is FinSequence-like Element of REAL *
f . S is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of Z
(n,Z,x,f,r,S) is V13() V16( NAT ) V17( REAL n) Function-like V32() FinSequence-like FinSubsequence-like complex-functions-valued ext-real-functions-valued real-functions-valued (n,Z,x,f . S)
(proj (Si,n)) * (n,Z,x,f,r,S) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
xseq is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
dom xseq is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
len (n,Z,x,f,r,S) is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
Seg (len (n,Z,x,f,r,S)) is V32() V39( len (n,Z,x,f,r,S)) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
seq is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len seq is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
Seg (len seq) is V32() V39( len seq) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom seq is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom (proj (Si,n)) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
K6((REAL n)) is set
rng x is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
rseqi is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset ((f . S),rseqi) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
x | (divset ((f . S),rseqi)) is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
rng (x | (divset ((f . S),rseqi))) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
(n,Z,x,f,r,S) . rseqi is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
vol (divset ((f . S),rseqi)) is V11() real ext-real Element of REAL
upper_bound (divset ((f . S),rseqi)) is V11() real ext-real Element of REAL
lower_bound (divset ((f . S),rseqi)) is V11() real ext-real Element of REAL
(upper_bound (divset ((f . S),rseqi))) - (lower_bound (divset ((f . S),rseqi))) is V11() real ext-real Element of REAL
k is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(vol (divset ((f . S),rseqi))) * k is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(proj (Si,n)) . k is V11() real ext-real Element of REAL
H is V11() real ext-real Element of REAL
dom (x | (divset ((f . S),rseqi))) is V129() V130() V131() Element of K6(Z)
K6(Z) is set
Fi is set
(x | (divset ((f . S),rseqi))) . Fi is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
dom x is V129() V130() V131() Element of K6(Z)
(dom x) /\ (divset ((f . S),rseqi)) is V129() V130() V131() Element of K6(REAL)
dom ((proj (Si,n)) * x) is V129() V130() V131() Element of K6(Z)
dom xs is V129() V130() V131() Element of K6(Z)
(dom xs) /\ (divset ((f . S),rseqi)) is V129() V130() V131() Element of K6(REAL)
xs | (divset ((f . S),rseqi)) is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
dom (xs | (divset ((f . S),rseqi))) is V129() V130() V131() Element of K6(Z)
x . Fi is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
(proj (Si,n)) . (x . Fi) is V11() real ext-real Element of REAL
((proj (Si,n)) * x) . Fi is V11() real ext-real Element of REAL
(xs | (divset ((f . S),rseqi))) . Fi is V11() real ext-real Element of REAL
z is V11() real ext-real Element of REAL
rng (xs | (divset ((f . S),rseqi))) is V129() V130() V131() Element of K6(REAL)
xseq . rseqi is V11() real ext-real Element of REAL
(proj (Si,n)) . ((n,Z,x,f,r,S) . rseqi) is V11() real ext-real Element of REAL
((vol (divset ((f . S),rseqi))) * k) . Si is V11() real ext-real Element of REAL
k . Si is V11() real ext-real Element of REAL
(vol (divset ((f . S),rseqi))) * (k . Si) is V11() real ext-real Element of REAL
z * (vol (divset ((f . S),rseqi))) is V11() real ext-real Element of REAL
len xseq is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
S is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (Z,xs,f)
(Z,xs,f,S) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
seq is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
xseq is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
seq . xseq is V11() real ext-real Element of REAL
rfz . xseq is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(rfz . xseq) . Si is V11() real ext-real Element of REAL
(n,Z,x,f,r,xseq) is V13() V16( NAT ) V17( REAL n) Function-like V32() FinSequence-like FinSubsequence-like complex-functions-valued ext-real-functions-valued real-functions-valued (n,Z,x,f . xseq)
f . xseq is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of Z
(proj (Si,n)) * (n,Z,x,f,r,xseq) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
(n,Z,x,(f . xseq),(n,Z,x,f,r,xseq)) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(n,Z,x,(f . xseq),(n,Z,x,f,r,xseq)) . Si is V11() real ext-real Element of REAL
(Z,xs,f,S,xseq) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (Z,xs,f . xseq)
(Z,xs,(f . xseq),(Z,xs,f,S,xseq)) is V11() real ext-real Element of REAL
Sum (Z,xs,f,S,xseq) is V11() real ext-real Element of REAL
rseqi is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum rseqi is V11() real ext-real Element of REAL
lim seq is V11() real ext-real Element of REAL
lim (Z,xs,f,S) is V11() real ext-real Element of REAL
integral xs is V11() real ext-real Element of REAL
upper_integral xs is V11() real ext-real Element of REAL
upper_sum_set xs is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set xs) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set xs)) is V11() real ext-real Element of REAL
xseq is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
seq . xseq is V11() real ext-real Element of REAL
rfz . xseq is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(rfz . xseq) . Si is V11() real ext-real Element of REAL
Si is Element of the carrier of (REAL-NS n)
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
(REAL n) * is non empty functional FinSequence-membered FinSequenceSet of REAL n
REAL-NS n is non empty V73() V194() V195() V196() V197() V198() V199() V200() V216() V217() strict V219() V225() L19()
Z is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
divs Z is non empty set
K7(NAT,(divs Z)) is V32() set
K6(K7(NAT,(divs Z))) is V32() set
x is non empty V13() V16(Z) V17( REAL n) Function-like total V27(Z, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
(n,Z,x) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
f is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
r is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
i is non empty V13() V16( NAT ) V17( divs Z) Function-like total V27( NAT , divs Z) Element of K6(K7(NAT,(divs Z)))
delta i is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (delta i) is V11() real ext-real Element of REAL
k is non empty V13() V16( NAT ) V17((REAL n) * ) Function-like total V27( NAT ,(REAL n) * ) (n,Z,x,i)
(n,Z,x,i,k) is V13() V16( NAT ) V17( the carrier of (REAL-NS n)) Function-like V27( NAT , the carrier of (REAL-NS n)) Element of K6(K7(NAT, the carrier of (REAL-NS n)))
the carrier of (REAL-NS n) is set
K7(NAT, the carrier of (REAL-NS n)) is set
K6(K7(NAT, the carrier of (REAL-NS n))) is set
lim (n,Z,x,i,k) is Element of the carrier of (REAL-NS n)
f is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
f is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
f . r is V11() real ext-real Element of REAL
Seg n is V32() V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * x is non empty V13() V16(Z) V17( REAL ) Function-like total V27(Z, REAL ) V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
rfz is non empty V13() V16( NAT ) V17( divs Z) Function-like total V27( NAT , divs Z) Element of K6(K7(NAT,(divs Z)))
Si is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (Z,(proj (r,n)) * x,rfz)
S is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
rfz . S is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of Z
(Z,((proj (r,n)) * x),rfz,Si,S) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (Z,(proj (r,n)) * x,rfz . S)
S is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len S is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
Seg (len S) is V32() V39( len S) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom (proj (r,n)) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
K6((REAL n)) is set
rng x is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
seq is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
xseq is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
dom S is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
divset ((rfz . S),xseq) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
((proj (r,n)) * x) | (divset ((rfz . S),xseq)) is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
rng (((proj (r,n)) * x) | (divset ((rfz . S),xseq))) is V129() V130() V131() Element of K6(REAL)
(Z,((proj (r,n)) * x),rfz,Si,S) . xseq is V11() real ext-real Element of REAL
vol (divset ((rfz . S),xseq)) is V11() real ext-real Element of REAL
upper_bound (divset ((rfz . S),xseq)) is V11() real ext-real Element of REAL
lower_bound (divset ((rfz . S),xseq)) is V11() real ext-real Element of REAL
(upper_bound (divset ((rfz . S),xseq))) - (lower_bound (divset ((rfz . S),xseq))) is V11() real ext-real Element of REAL
rseqi is V11() real ext-real Element of REAL
rseqi * (vol (divset ((rfz . S),xseq))) is V11() real ext-real Element of REAL
dom (((proj (r,n)) * x) | (divset ((rfz . S),xseq))) is V129() V130() V131() Element of K6(Z)
K6(Z) is set
k is set
(((proj (r,n)) * x) | (divset ((rfz . S),xseq))) . k is V11() real ext-real Element of REAL
dom ((proj (r,n)) * x) is V129() V130() V131() Element of K6(Z)
(dom ((proj (r,n)) * x)) /\ (divset ((rfz . S),xseq)) is V129() V130() V131() Element of K6(REAL)
x | (divset ((rfz . S),xseq)) is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
dom (x | (divset ((rfz . S),xseq))) is V129() V130() V131() Element of K6(Z)
dom x is V129() V130() V131() Element of K6(Z)
(dom x) /\ (divset ((rfz . S),xseq)) is V129() V130() V131() Element of K6(REAL)
H is V11() real ext-real Element of REAL
(x | (divset ((rfz . S),xseq))) . H is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
rng (x | (divset ((rfz . S),xseq))) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
z is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(vol (divset ((rfz . S),xseq))) * z is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
Fi is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
seq is V13() V16( NAT ) V17( REAL n) Function-like V32() FinSequence-like FinSubsequence-like complex-functions-valued ext-real-functions-valued real-functions-valued FinSequence of REAL n
dom seq is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
xseq is V13() V16( NAT ) V17( REAL n) Function-like V32() FinSequence-like FinSubsequence-like complex-functions-valued Element of (REAL n) *
rseqi is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
dom S is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
seq . k is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
divset ((rfz . S),rseqi) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
x | (divset ((rfz . S),rseqi)) is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
dom (x | (divset ((rfz . S),rseqi))) is V129() V130() V131() Element of K6(Z)
K6(Z) is set
(Z,((proj (r,n)) * x),rfz,Si,S) . rseqi is V11() real ext-real Element of REAL
vol (divset ((rfz . S),rseqi)) is V11() real ext-real Element of REAL
upper_bound (divset ((rfz . S),rseqi)) is V11() real ext-real Element of REAL
lower_bound (divset ((rfz . S),rseqi)) is V11() real ext-real Element of REAL
(upper_bound (divset ((rfz . S),rseqi))) - (lower_bound (divset ((rfz . S),rseqi))) is V11() real ext-real Element of REAL
((proj (r,n)) * x) | (divset ((rfz . S),rseqi)) is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
seq . rseqi is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
H is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
Fi is V11() real ext-real Element of REAL
divset ((rfz . S),H) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
x | (divset ((rfz . S),H)) is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
dom (x | (divset ((rfz . S),H))) is V129() V130() V131() Element of K6(Z)
(Z,((proj (r,n)) * x),rfz,Si,S) . H is V11() real ext-real Element of REAL
vol (divset ((rfz . S),H)) is V11() real ext-real Element of REAL
upper_bound (divset ((rfz . S),H)) is V11() real ext-real Element of REAL
lower_bound (divset ((rfz . S),H)) is V11() real ext-real Element of REAL
(upper_bound (divset ((rfz . S),H))) - (lower_bound (divset ((rfz . S),H))) is V11() real ext-real Element of REAL
((proj (r,n)) * x) | (divset ((rfz . S),H)) is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
(((proj (r,n)) * x) | (divset ((rfz . S),H))) . Fi is V11() real ext-real Element of REAL
(vol (divset ((rfz . S),H))) * ((((proj (r,n)) * x) | (divset ((rfz . S),H))) . Fi) is V11() real ext-real Element of REAL
z is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(x | (divset ((rfz . S),H))) . Fi is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
(vol (divset ((rfz . S),H))) * z is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
len seq is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
K7(NAT,((REAL n) *)) is V32() set
K6(K7(NAT,((REAL n) *))) is V32() set
S is non empty V13() V16( NAT ) V17((REAL n) * ) Function-like total V27( NAT ,(REAL n) * ) Element of K6(K7(NAT,((REAL n) *)))
S is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
S . S is FinSequence-like Element of (REAL n) *
rfz . S is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of Z
(Z,((proj (r,n)) * x),rfz,Si,S) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (Z,(proj (r,n)) * x,rfz . S)
seq is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
xseq is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len seq is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
len xseq is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
dom seq is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
rseqi is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
divset ((rfz . S),k) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
x | (divset ((rfz . S),k)) is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
dom (x | (divset ((rfz . S),k))) is V129() V130() V131() Element of K6(Z)
K6(Z) is set
(Z,((proj (r,n)) * x),rfz,Si,S) . k is V11() real ext-real Element of REAL
vol (divset ((rfz . S),k)) is V11() real ext-real Element of REAL
upper_bound (divset ((rfz . S),k)) is V11() real ext-real Element of REAL
lower_bound (divset ((rfz . S),k)) is V11() real ext-real Element of REAL
(upper_bound (divset ((rfz . S),k))) - (lower_bound (divset ((rfz . S),k))) is V11() real ext-real Element of REAL
((proj (r,n)) * x) | (divset ((rfz . S),k)) is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
xseq . k is set
z is V11() real ext-real Element of REAL
(((proj (r,n)) * x) | (divset ((rfz . S),k))) . z is V11() real ext-real Element of REAL
(vol (divset ((rfz . S),k))) * ((((proj (r,n)) * x) | (divset ((rfz . S),k))) . z) is V11() real ext-real Element of REAL
H is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(x | (divset ((rfz . S),k))) . z is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
(vol (divset ((rfz . S),k))) * H is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
Fi is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
divset ((rfz . S),rseqi) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
x | (divset ((rfz . S),rseqi)) is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
rng (x | (divset ((rfz . S),rseqi))) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
K6((REAL n)) is set
xseq . rseqi is set
vol (divset ((rfz . S),rseqi)) is V11() real ext-real Element of REAL
upper_bound (divset ((rfz . S),rseqi)) is V11() real ext-real Element of REAL
lower_bound (divset ((rfz . S),rseqi)) is V11() real ext-real Element of REAL
(upper_bound (divset ((rfz . S),rseqi))) - (lower_bound (divset ((rfz . S),rseqi))) is V11() real ext-real Element of REAL
(vol (divset ((rfz . S),rseqi))) * Fi is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
S is non empty V13() V16( NAT ) V17((REAL n) * ) Function-like total V27( NAT ,(REAL n) * ) (n,Z,x,rfz)
(n,Z,x,rfz,S) is V13() V16( NAT ) V17( the carrier of (REAL-NS n)) Function-like V27( NAT , the carrier of (REAL-NS n)) Element of K6(K7(NAT, the carrier of (REAL-NS n)))
the carrier of (REAL-NS n) is set
K7(NAT, the carrier of (REAL-NS n)) is set
K6(K7(NAT, the carrier of (REAL-NS n))) is set
K7(NAT,(REAL n)) is V32() set
K6(K7(NAT,(REAL n))) is V32() set
delta rfz is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (delta rfz) is V11() real ext-real Element of REAL
lim (n,Z,x,rfz,S) is Element of the carrier of (REAL-NS n)
xseq is non empty V13() V16( NAT ) V17( REAL n) Function-like total V27( NAT , REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(NAT,(REAL n)))
xs is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
xs . r is V11() real ext-real Element of REAL
rseqi is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim rseqi is V11() real ext-real Element of REAL
(Z,((proj (r,n)) * x),rfz,Si) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
rseqi . k is V11() real ext-real Element of REAL
(Z,((proj (r,n)) * x),rfz,Si) . k is V11() real ext-real Element of REAL
rfz . k is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of Z
(n,Z,x,rfz,S,k) is V13() V16( NAT ) V17( REAL n) Function-like V32() FinSequence-like FinSubsequence-like complex-functions-valued ext-real-functions-valued real-functions-valued (n,Z,x,rfz . k)
(Z,((proj (r,n)) * x),rfz,Si,k) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (Z,(proj (r,n)) * x,rfz . k)
H is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
z is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len H is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
len z is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
dom H is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom (proj (r,n)) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
K6((REAL n)) is set
rng (n,Z,x,rfz,S,k) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
(proj (r,n)) * (n,Z,x,rfz,S,k) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
dom ((proj (r,n)) * (n,Z,x,rfz,S,k)) is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom (n,Z,x,rfz,S,k) is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
Seg (len H) is V32() V39( len H) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
len (Z,((proj (r,n)) * x),rfz,Si,k) is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
Seg (len (Z,((proj (r,n)) * x),rfz,Si,k)) is V32() V39( len (Z,((proj (r,n)) * x),rfz,Si,k)) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom (Z,((proj (r,n)) * x),rfz,Si,k) is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
Fi is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
((proj (r,n)) * (n,Z,x,rfz,S,k)) . Fi is V11() real ext-real Element of REAL
(Z,((proj (r,n)) * x),rfz,Si,k) . Fi is V11() real ext-real Element of REAL
rng x is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
j is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
divset ((rfz . k),j) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
x | (divset ((rfz . k),j)) is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
dom (x | (divset ((rfz . k),j))) is V129() V130() V131() Element of K6(Z)
K6(Z) is set
(Z,((proj (r,n)) * x),rfz,Si,k) . j is V11() real ext-real Element of REAL
vol (divset ((rfz . k),j)) is V11() real ext-real Element of REAL
upper_bound (divset ((rfz . k),j)) is V11() real ext-real Element of REAL
lower_bound (divset ((rfz . k),j)) is V11() real ext-real Element of REAL
(upper_bound (divset ((rfz . k),j))) - (lower_bound (divset ((rfz . k),j))) is V11() real ext-real Element of REAL
((proj (r,n)) * x) | (divset ((rfz . k),j)) is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
z . j is set
tji is V11() real ext-real Element of REAL
(((proj (r,n)) * x) | (divset ((rfz . k),j))) . tji is V11() real ext-real Element of REAL
(vol (divset ((rfz . k),j))) * ((((proj (r,n)) * x) | (divset ((rfz . k),j))) . tji) is V11() real ext-real Element of REAL
rji is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(x | (divset ((rfz . k),j))) . tji is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
(vol (divset ((rfz . k),j))) * rji is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
dom x is V129() V130() V131() Element of K6(Z)
(dom x) /\ (divset ((rfz . k),j)) is V129() V130() V131() Element of K6(REAL)
dom ((proj (r,n)) * x) is V129() V130() V131() Element of K6(Z)
(dom ((proj (r,n)) * x)) /\ (divset ((rfz . k),j)) is V129() V130() V131() Element of K6(REAL)
dom (((proj (r,n)) * x) | (divset ((rfz . k),j))) is V129() V130() V131() Element of K6(Z)
((proj (r,n)) * x) . tji is V11() real ext-real Element of REAL
x . tji is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
(proj (r,n)) . (x . tji) is V11() real ext-real Element of REAL
(proj (r,n)) . rji is V11() real ext-real Element of REAL
((proj (r,n)) * (n,Z,x,rfz,S,k)) . j is V11() real ext-real Element of REAL
(n,Z,x,rfz,S,k) . j is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
(proj (r,n)) . ((n,Z,x,rfz,S,k) . j) is V11() real ext-real Element of REAL
((vol (divset ((rfz . k),j))) * rji) . r is V11() real ext-real Element of REAL
rji . r is V11() real ext-real Element of REAL
(vol (divset ((rfz . k),j))) * (rji . r) is V11() real ext-real Element of REAL
(n,Z,x,(rfz . k),(n,Z,x,rfz,S,k)) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(n,Z,x,(rfz . k),(n,Z,x,rfz,S,k)) . r is V11() real ext-real Element of REAL
Fi is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum Fi is V11() real ext-real Element of REAL
xseq . k is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(xseq . k) . r is V11() real ext-real Element of REAL
(Z,((proj (r,n)) * x),(rfz . k),(Z,((proj (r,n)) * x),rfz,Si,k)) is V11() real ext-real Element of REAL
Sum (Z,((proj (r,n)) * x),rfz,Si,k) is V11() real ext-real Element of REAL
lim (Z,((proj (r,n)) * x),rfz,Si) is V11() real ext-real Element of REAL
i is V11() real ext-real Element of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is V32() set
K6(K7(REAL,(REAL n))) is V32() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is V32() set
K6(K7(REAL,(REAL n))) is V32() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is V32() set
K6(K7(REAL,(REAL n))) is V32() set
Seg n is V32() V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
Z is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
x is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (r,n)) * x),Z) is V11() real ext-real Element of REAL
((proj (r,n)) * x) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
integral (((proj (r,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * x) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
divs Z is non empty set
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set (((proj (r,n)) * x) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * x) || Z))) is V11() real ext-real Element of REAL
i is V11() real ext-real Element of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
dom f is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
f . r is V11() real ext-real Element of REAL
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (r,n)) * x),Z) is V11() real ext-real Element of REAL
((proj (r,n)) * x) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
integral (((proj (r,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * x) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
divs Z is non empty set
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set (((proj (r,n)) * x) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * x) || Z))) is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (i,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
(proj (i,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (i,n)) * x),Z) is V11() real ext-real Element of REAL
((proj (i,n)) * x) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
integral (((proj (i,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (i,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (i,n)) * x) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
rng (upper_sum_set (((proj (i,n)) * x) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (i,n)) * x) || Z))) is V11() real ext-real Element of REAL
len f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
f . r is V11() real ext-real Element of REAL
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (r,n)) * x),Z) is V11() real ext-real Element of REAL
((proj (r,n)) * x) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
integral (((proj (r,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * x) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
divs Z is non empty set
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set (((proj (r,n)) * x) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * x) || Z))) is V11() real ext-real Element of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
dom f is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
dom r is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
f . i is V11() real ext-real Element of REAL
r . i is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
r . k is V11() real ext-real Element of REAL
proj (k,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (k,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (k,n)) * x),Z) is V11() real ext-real Element of REAL
((proj (k,n)) * x) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
integral (((proj (k,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (k,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (k,n)) * x) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
divs Z is non empty set
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set (((proj (k,n)) * x) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (k,n)) * x) || Z))) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is V32() set
K6(K7(REAL,(REAL n))) is V32() set
Z is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
x is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
x | Z is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
f is non empty V13() V16(Z) V17( REAL n) Function-like total V27(Z, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
Seg n is V32() V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * f is non empty V13() V16(Z) V17( REAL ) Function-like total V27(Z, REAL ) V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
dom (proj (r,n)) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
K6((REAL n)) is set
rng x is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
(proj (r,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
dom ((proj (r,n)) * x) is V129() V130() V131() Element of K6(REAL)
dom x is V129() V130() V131() Element of K6(REAL)
dom f is V129() V130() V131() Element of K6(Z)
K6(Z) is set
(dom x) /\ Z is V129() V130() V131() Element of K6(REAL)
((proj (r,n)) * x) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
((proj (r,n)) * x) | Z is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
i is non empty V13() V16(Z) V17( REAL ) Function-like total V27(Z, REAL ) V119() V120() V121() Element of K6(K7(Z,REAL))
Seg n is V32() V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
(proj (r,n)) * f is non empty V13() V16(Z) V17( REAL ) Function-like total V27(Z, REAL ) V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
((proj (r,n)) * x) | Z is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
((proj (r,n)) * x) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is V32() set
K6(K7(REAL,(REAL n))) is V32() set
Z is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
x is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
x | Z is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
(n,Z,x) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
f is non empty V13() V16(Z) V17( REAL n) Function-like total V27(Z, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
(n,Z,f) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
dom (n,Z,x) is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (i,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
dom (proj (i,n)) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
K6((REAL n)) is set
rng x is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
(proj (i,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
dom ((proj (i,n)) * x) is V129() V130() V131() Element of K6(REAL)
dom x is V129() V130() V131() Element of K6(REAL)
dom f is V129() V130() V131() Element of K6(Z)
K6(Z) is set
(dom x) /\ Z is V129() V130() V131() Element of K6(REAL)
((proj (i,n)) * x) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
((proj (i,n)) * x) | Z is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
k is non empty V13() V16(Z) V17( REAL ) Function-like total V27(Z, REAL ) V119() V120() V121() Element of K6(K7(Z,REAL))
(proj (i,n)) * f is non empty V13() V16(Z) V17( REAL ) Function-like total V27(Z, REAL ) V119() V120() V121() Element of K6(K7(Z,REAL))
Seg n is V32() V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
(n,Z,x) . i is V11() real ext-real Element of REAL
integral (((proj (i,n)) * x),Z) is V11() real ext-real Element of REAL
integral (((proj (i,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (i,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (i,n)) * x) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
divs Z is non empty set
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set (((proj (i,n)) * x) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (i,n)) * x) || Z))) is V11() real ext-real Element of REAL
(n,Z,x) . r is V11() real ext-real Element of REAL
(n,Z,f) . r is V11() real ext-real Element of REAL
dom (n,Z,f) is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
x is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL x is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
x -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL x)) is V32() set
K6(K7(REAL,(REAL x))) is V32() set
Seg x is V32() V39(x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
n is V11() real ext-real set
Z is V11() real ext-real set
f is V13() V16( REAL ) V17( REAL x) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL x)))
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (i,x) is non empty V13() V16( REAL x) V17( REAL ) Function-like total V27( REAL x, REAL ) V119() V120() V121() Element of K6(K7((REAL x),REAL))
K7((REAL x),REAL) is V32() V119() V120() V121() set
K6(K7((REAL x),REAL)) is V32() set
(proj (i,x)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (i,x)) * f),n,Z) is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
r is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
dom r is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
r . i is V11() real ext-real Element of REAL
proj (i,x) is non empty V13() V16( REAL x) V17( REAL ) Function-like total V27( REAL x, REAL ) V119() V120() V121() Element of K6(K7((REAL x),REAL))
K7((REAL x),REAL) is V32() V119() V120() V121() set
K6(K7((REAL x),REAL)) is V32() set
(proj (i,x)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (i,x)) * f),n,Z) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (k,x) is non empty V13() V16( REAL x) V17( REAL ) Function-like total V27( REAL x, REAL ) V119() V120() V121() Element of K6(K7((REAL x),REAL))
(proj (k,x)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (k,x)) * f),n,Z) is V11() real ext-real Element of REAL
len r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
r . i is V11() real ext-real Element of REAL
proj (i,x) is non empty V13() V16( REAL x) V17( REAL ) Function-like total V27( REAL x, REAL ) V119() V120() V121() Element of K6(K7((REAL x),REAL))
K7((REAL x),REAL) is V32() V119() V120() V121() set
K6(K7((REAL x),REAL)) is V32() set
(proj (i,x)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (i,x)) * f),n,Z) is V11() real ext-real Element of REAL
r is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL x
dom r is V39(x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
i is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL x
dom i is V39(x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
r . k is V11() real ext-real Element of REAL
i . k is V11() real ext-real Element of REAL
rfz is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
i . rfz is V11() real ext-real Element of REAL
proj (rfz,x) is non empty V13() V16( REAL x) V17( REAL ) Function-like total V27( REAL x, REAL ) V119() V120() V121() Element of K6(K7((REAL x),REAL))
K7((REAL x),REAL) is V32() V119() V120() V121() set
K6(K7((REAL x),REAL)) is V32() set
(proj (rfz,x)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (rfz,x)) * f),n,Z) is V11() real ext-real Element of REAL
n is set
Z is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL Z is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
Z -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(n,(REAL Z)) is set
K6(K7(n,(REAL Z))) is set
x is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (x,Z) is non empty V13() V16( REAL Z) V17( REAL ) Function-like total V27( REAL Z, REAL ) V119() V120() V121() Element of K6(K7((REAL Z),REAL))
K7((REAL Z),REAL) is V32() V119() V120() V121() set
K6(K7((REAL Z),REAL)) is V32() set
f is V13() V16(n) V17( REAL Z) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(n,(REAL Z)))
r is V13() V16(n) V17( REAL Z) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(n,(REAL Z)))
(Z,n,f,r) is V13() V16(n) V17( REAL Z) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(n,(REAL Z)))
f <++> r is V13() V16(n /\ n) V17( R_PFuncs ((DOMS (REAL Z)) /\ (DOMS (REAL Z)))) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((n /\ n),(R_PFuncs ((DOMS (REAL Z)) /\ (DOMS (REAL Z))))))
n /\ n is set
DOMS (REAL Z) is set
(DOMS (REAL Z)) /\ (DOMS (REAL Z)) is set
R_PFuncs ((DOMS (REAL Z)) /\ (DOMS (REAL Z))) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K7((n /\ n),(R_PFuncs ((DOMS (REAL Z)) /\ (DOMS (REAL Z))))) is set
K6(K7((n /\ n),(R_PFuncs ((DOMS (REAL Z)) /\ (DOMS (REAL Z)))))) is set
(proj (x,Z)) * (Z,n,f,r) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
K7(n,REAL) is V119() V120() V121() set
K6(K7(n,REAL)) is set
(proj (x,Z)) * f is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
(proj (x,Z)) * r is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
((proj (x,Z)) * f) + ((proj (x,Z)) * r) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
(Z,n,f,r) is V13() V16(n) V17( REAL Z) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(n,(REAL Z)))
f <--> r is V13() V16(n /\ n) V17( R_PFuncs ((DOMS (REAL Z)) /\ (DOMS (REAL Z)))) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((n /\ n),(R_PFuncs ((DOMS (REAL Z)) /\ (DOMS (REAL Z))))))
(proj (x,Z)) * (Z,n,f,r) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
((proj (x,Z)) * f) - ((proj (x,Z)) * r) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
dom (proj (x,Z)) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL Z))
K6((REAL Z)) is set
rng f is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL Z))
dom ((proj (x,Z)) * f) is Element of K6(n)
K6(n) is set
dom f is Element of K6(n)
rng (Z,n,f,r) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL Z))
dom ((proj (x,Z)) * (Z,n,f,r)) is Element of K6(n)
dom (Z,n,f,r) is Element of K6(n)
rng r is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL Z))
dom ((proj (x,Z)) * r) is Element of K6(n)
dom r is Element of K6(n)
(dom f) /\ (dom r) is Element of K6(n)
i is Element of n
((proj (x,Z)) * (Z,n,f,r)) . i is V11() real ext-real Element of REAL
(((proj (x,Z)) * f) + ((proj (x,Z)) * r)) . i is V11() real ext-real Element of REAL
f /. i is V39(Z) FinSequence-like V119() V120() V121() Element of REAL Z
r /. i is V39(Z) FinSequence-like V119() V120() V121() Element of REAL Z
f . i is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
k is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(Z) FinSequence-like FinSubsequence-like V119() V120() V121() Element of Z -tuples_on REAL
r . i is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
rfz is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(Z) FinSequence-like FinSubsequence-like V119() V120() V121() Element of Z -tuples_on REAL
(Z,n,f,r) . i is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
(proj (x,Z)) . ((Z,n,f,r) . i) is V11() real ext-real Element of REAL
(f . i) + (r . i) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
(proj (x,Z)) . ((f . i) + (r . i)) is V11() real ext-real Element of REAL
(f /. i) + (r /. i) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(Z) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL Z
((f /. i) + (r /. i)) . x is V11() real ext-real Element of REAL
k . x is V11() real ext-real Element of REAL
rfz . x is V11() real ext-real Element of REAL
(k . x) + (rfz . x) is V11() real ext-real Element of REAL
(dom ((proj (x,Z)) * f)) /\ (dom ((proj (x,Z)) * r)) is Element of K6(n)
((proj (x,Z)) * f) . i is V11() real ext-real Element of REAL
(proj (x,Z)) . (f . i) is V11() real ext-real Element of REAL
((proj (x,Z)) * r) . i is V11() real ext-real Element of REAL
(proj (x,Z)) . (r . i) is V11() real ext-real Element of REAL
dom (((proj (x,Z)) * f) + ((proj (x,Z)) * r)) is Element of K6(n)
dom (((proj (x,Z)) * f) + ((proj (x,Z)) * r)) is Element of K6(n)
rng (Z,n,f,r) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL Z))
dom ((proj (x,Z)) * (Z,n,f,r)) is Element of K6(n)
dom (Z,n,f,r) is Element of K6(n)
dom (((proj (x,Z)) * f) - ((proj (x,Z)) * r)) is Element of K6(n)
i is Element of n
((proj (x,Z)) * (Z,n,f,r)) . i is V11() real ext-real Element of REAL
(((proj (x,Z)) * f) - ((proj (x,Z)) * r)) . i is V11() real ext-real Element of REAL
f /. i is V39(Z) FinSequence-like V119() V120() V121() Element of REAL Z
r /. i is V39(Z) FinSequence-like V119() V120() V121() Element of REAL Z
f . i is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
k is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(Z) FinSequence-like FinSubsequence-like V119() V120() V121() Element of Z -tuples_on REAL
r . i is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
rfz is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(Z) FinSequence-like FinSubsequence-like V119() V120() V121() Element of Z -tuples_on REAL
((proj (x,Z)) * r) . i is V11() real ext-real Element of REAL
(proj (x,Z)) . (r . i) is V11() real ext-real Element of REAL
rfz . x is V11() real ext-real Element of REAL
(Z,n,f,r) . i is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
(proj (x,Z)) . ((Z,n,f,r) . i) is V11() real ext-real Element of REAL
(f . i) - (r . i) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
(proj (x,Z)) . ((f . i) - (r . i)) is V11() real ext-real Element of REAL
(f /. i) - (r /. i) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(Z) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL Z
((f /. i) - (r /. i)) . x is V11() real ext-real Element of REAL
k . x is V11() real ext-real Element of REAL
(k . x) - (rfz . x) is V11() real ext-real Element of REAL
((proj (x,Z)) * f) . i is V11() real ext-real Element of REAL
(proj (x,Z)) . (f . i) is V11() real ext-real Element of REAL
(((proj (x,Z)) * f) . i) - (((proj (x,Z)) * r) . i) is V11() real ext-real Element of REAL
n is set
Z is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL Z is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
Z -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(n,(REAL Z)) is set
K6(K7(n,(REAL Z))) is set
x is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (x,Z) is non empty V13() V16( REAL Z) V17( REAL ) Function-like total V27( REAL Z, REAL ) V119() V120() V121() Element of K6(K7((REAL Z),REAL))
K7((REAL Z),REAL) is V32() V119() V120() V121() set
K6(K7((REAL Z),REAL)) is V32() set
f is V11() real ext-real Element of REAL
r is V13() V16(n) V17( REAL Z) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(n,(REAL Z)))
(Z,f,n,r) is V13() V16(n) V17( REAL Z) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(n,(REAL Z)))
r [#] f is V13() V16(n) V17( R_PFuncs (DOMS (REAL Z))) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(n,(R_PFuncs (DOMS (REAL Z)))))
DOMS (REAL Z) is set
R_PFuncs (DOMS (REAL Z)) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K7(n,(R_PFuncs (DOMS (REAL Z)))) is set
K6(K7(n,(R_PFuncs (DOMS (REAL Z))))) is set
(proj (x,Z)) * (Z,f,n,r) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
K7(n,REAL) is V119() V120() V121() set
K6(K7(n,REAL)) is set
(proj (x,Z)) * r is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
f (#) ((proj (x,Z)) * r) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
dom (Z,f,n,r) is Element of K6(n)
K6(n) is set
dom r is Element of K6(n)
dom (proj (x,Z)) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL Z))
K6((REAL Z)) is set
rng (Z,f,n,r) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL Z))
rng r is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL Z))
dom ((proj (x,Z)) * r) is Element of K6(n)
dom (f (#) ((proj (x,Z)) * r)) is Element of K6(n)
dom ((proj (x,Z)) * (Z,f,n,r)) is Element of K6(n)
i is Element of n
((proj (x,Z)) * (Z,f,n,r)) . i is V11() real ext-real Element of REAL
(f (#) ((proj (x,Z)) * r)) . i is V11() real ext-real Element of REAL
r /. i is V39(Z) FinSequence-like V119() V120() V121() Element of REAL Z
(Z,f,n,r) /. i is V39(Z) FinSequence-like V119() V120() V121() Element of REAL Z
r . i is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
k is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(Z) FinSequence-like FinSubsequence-like V119() V120() V121() Element of Z -tuples_on REAL
((proj (x,Z)) * r) . i is V11() real ext-real Element of REAL
f * (((proj (x,Z)) * r) . i) is V11() real ext-real Element of REAL
(proj (x,Z)) . k is V11() real ext-real Element of REAL
f * ((proj (x,Z)) . k) is V11() real ext-real Element of REAL
k . x is V11() real ext-real Element of REAL
f * (k . x) is V11() real ext-real Element of REAL
(Z,f,n,r) . i is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
rfz is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(Z) FinSequence-like FinSubsequence-like V119() V120() V121() Element of Z -tuples_on REAL
(proj (x,Z)) . ((Z,f,n,r) . i) is V11() real ext-real Element of REAL
rfz . x is V11() real ext-real Element of REAL
f (#) k is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() Element of K6(K7(NAT,REAL))
(f (#) k) . x is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is V32() set
K6(K7(REAL,(REAL n))) is V32() set
Z is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
x is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
f is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
dom x is V129() V130() V131() Element of K6(REAL)
dom f is V129() V130() V131() Element of K6(REAL)
x | Z is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
f | Z is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
(n,REAL,x,f) is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
x <++> f is V13() V16(REAL /\ REAL) V17( R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL /\ REAL),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))))
REAL /\ REAL is V129() V130() V131() set
DOMS (REAL n) is set
(DOMS (REAL n)) /\ (DOMS (REAL n)) is set
R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K7((REAL /\ REAL),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))) is set
K6(K7((REAL /\ REAL),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))))) is set
(n,REAL,x,f) is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
x <--> f is V13() V16(REAL /\ REAL) V17( R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL /\ REAL),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))))
(n,Z,(n,REAL,x,f)) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(n,Z,x) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(n,Z,f) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(n,Z,x) + (n,Z,f) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(n,Z,(n,REAL,x,f)) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(n,Z,x) - (n,Z,f) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
Seg n is V32() V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
dom ((proj (r,n)) * x) is V129() V130() V131() Element of K6(REAL)
(proj (r,n)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
dom ((proj (r,n)) * f) is V129() V130() V131() Element of K6(REAL)
dom (proj (r,n)) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
K6((REAL n)) is set
rng x is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
rng f is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
(proj (r,n)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
((proj (r,n)) * x) + ((proj (r,n)) * f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral ((((proj (r,n)) * x) + ((proj (r,n)) * f)),Z) is V11() real ext-real Element of REAL
(((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
integral ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z) is V11() real ext-real Element of REAL
upper_integral ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z) is V11() real ext-real Element of REAL
upper_sum_set ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
divs Z is non empty set
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z))) is V11() real ext-real Element of REAL
integral (((proj (r,n)) * x),Z) is V11() real ext-real Element of REAL
((proj (r,n)) * x) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
integral (((proj (r,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * x) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
rng (upper_sum_set (((proj (r,n)) * x) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * x) || Z))) is V11() real ext-real Element of REAL
integral (((proj (r,n)) * f),Z) is V11() real ext-real Element of REAL
((proj (r,n)) * f) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
integral (((proj (r,n)) * f) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * f) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * f) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
rng (upper_sum_set (((proj (r,n)) * f) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * f) || Z))) is V11() real ext-real Element of REAL
(integral (((proj (r,n)) * x),Z)) + (integral (((proj (r,n)) * f),Z)) is V11() real ext-real Element of REAL
((proj (r,n)) * x) - ((proj (r,n)) * f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral ((((proj (r,n)) * x) - ((proj (r,n)) * f)),Z) is V11() real ext-real Element of REAL
(((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
integral ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z) is V11() real ext-real Element of REAL
upper_integral ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z) is V11() real ext-real Element of REAL
upper_sum_set ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
rng (upper_sum_set ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z))) is V11() real ext-real Element of REAL
(integral (((proj (r,n)) * x),Z)) - (integral (((proj (r,n)) * f),Z)) is V11() real ext-real Element of REAL
dom ((proj (r,n)) * x) is V129() V130() V131() Element of K6(REAL)
dom ((proj (r,n)) * f) is V129() V130() V131() Element of K6(REAL)
(proj (r,n)) * (f | Z) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
((proj (r,n)) * f) | Z is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
(proj (r,n)) * (x | Z) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
((proj (r,n)) * x) | Z is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * (n,REAL,x,f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
(proj (r,n)) * (n,REAL,x,f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
(proj (r,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
(proj (r,n)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
((proj (r,n)) * x) + ((proj (r,n)) * f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
((proj (r,n)) * x) - ((proj (r,n)) * f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * (n,REAL,x,f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,x) . r is V11() real ext-real Element of REAL
(n,Z,f) . r is V11() real ext-real Element of REAL
((n,Z,x) . r) + ((n,Z,f) . r) is V11() real ext-real Element of REAL
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (r,n)) * x),Z) is V11() real ext-real Element of REAL
((proj (r,n)) * x) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
integral (((proj (r,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * x) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
divs Z is non empty set
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set (((proj (r,n)) * x) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * x) || Z))) is V11() real ext-real Element of REAL
(proj (r,n)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (r,n)) * f),Z) is V11() real ext-real Element of REAL
((proj (r,n)) * f) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
integral (((proj (r,n)) * f) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * f) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * f) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
rng (upper_sum_set (((proj (r,n)) * f) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * f) || Z))) is V11() real ext-real Element of REAL
(integral (((proj (r,n)) * x),Z)) + (integral (((proj (r,n)) * f),Z)) is V11() real ext-real Element of REAL
((n,Z,x) . r) - ((n,Z,f) . r) is V11() real ext-real Element of REAL
(integral (((proj (r,n)) * x),Z)) - (integral (((proj (r,n)) * f),Z)) is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,x) . r is V11() real ext-real Element of REAL
(n,Z,f) . r is V11() real ext-real Element of REAL
((n,Z,x) . r) + ((n,Z,f) . r) is V11() real ext-real Element of REAL
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
(proj (r,n)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
((proj (r,n)) * x) + ((proj (r,n)) * f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral ((((proj (r,n)) * x) + ((proj (r,n)) * f)),Z) is V11() real ext-real Element of REAL
(((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
integral ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z) is V11() real ext-real Element of REAL
upper_integral ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z) is V11() real ext-real Element of REAL
upper_sum_set ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
divs Z is non empty set
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z))) is V11() real ext-real Element of REAL
((n,Z,x) . r) - ((n,Z,f) . r) is V11() real ext-real Element of REAL
((proj (r,n)) * x) - ((proj (r,n)) * f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral ((((proj (r,n)) * x) - ((proj (r,n)) * f)),Z) is V11() real ext-real Element of REAL
(((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
integral ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z) is V11() real ext-real Element of REAL
upper_integral ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z) is V11() real ext-real Element of REAL
upper_sum_set ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
rng (upper_sum_set ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z))) is V11() real ext-real Element of REAL
integral (((proj (r,n)) * x),Z) is V11() real ext-real Element of REAL
((proj (r,n)) * x) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
integral (((proj (r,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * x) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * x) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
rng (upper_sum_set (((proj (r,n)) * x) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * x) || Z))) is V11() real ext-real Element of REAL
integral (((proj (r,n)) * f),Z) is V11() real ext-real Element of REAL
((proj (r,n)) * f) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
integral (((proj (r,n)) * f) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * f) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * f) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
rng (upper_sum_set (((proj (r,n)) * f) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * f) || Z))) is V11() real ext-real Element of REAL
(integral (((proj (r,n)) * x),Z)) + (integral (((proj (r,n)) * f),Z)) is V11() real ext-real Element of REAL
(integral (((proj (r,n)) * x),Z)) - (integral (((proj (r,n)) * f),Z)) is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,x) . r is V11() real ext-real Element of REAL
(n,Z,f) . r is V11() real ext-real Element of REAL
((n,Z,x) . r) + ((n,Z,f) . r) is V11() real ext-real Element of REAL
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * (n,REAL,x,f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (r,n)) * (n,REAL,x,f)),Z) is V11() real ext-real Element of REAL
((proj (r,n)) * (n,REAL,x,f)) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
integral (((proj (r,n)) * (n,REAL,x,f)) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * (n,REAL,x,f)) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * (n,REAL,x,f)) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
divs Z is non empty set
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set (((proj (r,n)) * (n,REAL,x,f)) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * (n,REAL,x,f)) || Z))) is V11() real ext-real Element of REAL
((n,Z,x) . r) - ((n,Z,f) . r) is V11() real ext-real Element of REAL
(proj (r,n)) * (n,REAL,x,f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (r,n)) * (n,REAL,x,f)),Z) is V11() real ext-real Element of REAL
((proj (r,n)) * (n,REAL,x,f)) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
integral (((proj (r,n)) * (n,REAL,x,f)) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * (n,REAL,x,f)) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * (n,REAL,x,f)) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
rng (upper_sum_set (((proj (r,n)) * (n,REAL,x,f)) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * (n,REAL,x,f)) || Z))) is V11() real ext-real Element of REAL
(proj (r,n)) * x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
(proj (r,n)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
((proj (r,n)) * x) + ((proj (r,n)) * f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral ((((proj (r,n)) * x) + ((proj (r,n)) * f)),Z) is V11() real ext-real Element of REAL
(((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
integral ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z) is V11() real ext-real Element of REAL
upper_integral ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z) is V11() real ext-real Element of REAL
upper_sum_set ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
rng (upper_sum_set ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((((proj (r,n)) * x) + ((proj (r,n)) * f)) || Z))) is V11() real ext-real Element of REAL
((proj (r,n)) * x) - ((proj (r,n)) * f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral ((((proj (r,n)) * x) - ((proj (r,n)) * f)),Z) is V11() real ext-real Element of REAL
(((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
integral ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z) is V11() real ext-real Element of REAL
upper_integral ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z) is V11() real ext-real Element of REAL
upper_sum_set ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
rng (upper_sum_set ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((((proj (r,n)) * x) - ((proj (r,n)) * f)) || Z))) is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,(n,REAL,x,f)) . r is V11() real ext-real Element of REAL
(n,Z,x) . r is V11() real ext-real Element of REAL
(n,Z,f) . r is V11() real ext-real Element of REAL
((n,Z,x) . r) + ((n,Z,f) . r) is V11() real ext-real Element of REAL
(n,Z,(n,REAL,x,f)) . r is V11() real ext-real Element of REAL
((n,Z,x) . r) - ((n,Z,f) . r) is V11() real ext-real Element of REAL
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * (n,REAL,x,f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (r,n)) * (n,REAL,x,f)),Z) is V11() real ext-real Element of REAL
((proj (r,n)) * (n,REAL,x,f)) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
K7(Z,REAL) is V32() V119() V120() V121() set
K6(K7(Z,REAL)) is V32() set
integral (((proj (r,n)) * (n,REAL,x,f)) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * (n,REAL,x,f)) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * (n,REAL,x,f)) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
divs Z is non empty set
K7((divs Z),REAL) is V32() V119() V120() V121() set
K6(K7((divs Z),REAL)) is V32() set
rng (upper_sum_set (((proj (r,n)) * (n,REAL,x,f)) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * (n,REAL,x,f)) || Z))) is V11() real ext-real Element of REAL
(proj (r,n)) * (n,REAL,x,f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (r,n)) * (n,REAL,x,f)),Z) is V11() real ext-real Element of REAL
((proj (r,n)) * (n,REAL,x,f)) || Z is V13() V16(Z) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(Z,REAL))
integral (((proj (r,n)) * (n,REAL,x,f)) || Z) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * (n,REAL,x,f)) || Z) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * (n,REAL,x,f)) || Z) is non empty V13() V16( divs Z) V17( REAL ) Function-like total V27( divs Z, REAL ) V119() V120() V121() Element of K6(K7((divs Z),REAL))
rng (upper_sum_set (((proj (r,n)) * (n,REAL,x,f)) || Z)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * (n,REAL,x,f)) || Z))) is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (r,n)) * (n,REAL,x,f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
dom (n,Z,(n,REAL,x,f)) is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,(n,REAL,x,f)) . r is V11() real ext-real Element of REAL
((n,Z,x) + (n,Z,f)) . r is V11() real ext-real Element of REAL
(n,Z,x) . r is V11() real ext-real Element of REAL
(n,Z,f) . r is V11() real ext-real Element of REAL
((n,Z,x) . r) + ((n,Z,f) . r) is V11() real ext-real Element of REAL
dom ((n,Z,x) + (n,Z,f)) is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom (n,Z,(n,REAL,x,f)) is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,(n,REAL,x,f)) . r is V11() real ext-real Element of REAL
((n,Z,x) - (n,Z,f)) . r is V11() real ext-real Element of REAL
(n,Z,x) . r is V11() real ext-real Element of REAL
(n,Z,f) . r is V11() real ext-real Element of REAL
((n,Z,x) . r) - ((n,Z,f) . r) is V11() real ext-real Element of REAL
dom ((n,Z,x) - (n,Z,f)) is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is V32() set
K6(K7(REAL,(REAL n))) is V32() set
Z is V11() real ext-real Element of REAL
x is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
f is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
dom f is V129() V130() V131() Element of K6(REAL)
f | x is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
(n,Z,REAL,f) is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
f [#] Z is V13() V16( REAL ) V17( R_PFuncs (DOMS (REAL n))) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(R_PFuncs (DOMS (REAL n)))))
DOMS (REAL n) is set
R_PFuncs (DOMS (REAL n)) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K7(REAL,(R_PFuncs (DOMS (REAL n)))) is set
K6(K7(REAL,(R_PFuncs (DOMS (REAL n))))) is set
(n,x,(n,Z,REAL,f)) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
(n,x,f) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
Z * (n,x,f) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
dom (proj (r,n)) is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
K6((REAL n)) is set
rng f is functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL n))
(proj (r,n)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
dom ((proj (r,n)) * f) is V129() V130() V131() Element of K6(REAL)
Seg n is V32() V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
(proj (r,n)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
Z (#) ((proj (r,n)) * f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral ((Z (#) ((proj (r,n)) * f)),x) is V11() real ext-real Element of REAL
(Z (#) ((proj (r,n)) * f)) || x is V13() V16(x) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(x,REAL))
K7(x,REAL) is V32() V119() V120() V121() set
K6(K7(x,REAL)) is V32() set
integral ((Z (#) ((proj (r,n)) * f)) || x) is V11() real ext-real Element of REAL
upper_integral ((Z (#) ((proj (r,n)) * f)) || x) is V11() real ext-real Element of REAL
upper_sum_set ((Z (#) ((proj (r,n)) * f)) || x) is non empty V13() V16( divs x) V17( REAL ) Function-like total V27( divs x, REAL ) V119() V120() V121() Element of K6(K7((divs x),REAL))
divs x is non empty set
K7((divs x),REAL) is V32() V119() V120() V121() set
K6(K7((divs x),REAL)) is V32() set
rng (upper_sum_set ((Z (#) ((proj (r,n)) * f)) || x)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((Z (#) ((proj (r,n)) * f)) || x))) is V11() real ext-real Element of REAL
integral (((proj (r,n)) * f),x) is V11() real ext-real Element of REAL
((proj (r,n)) * f) || x is V13() V16(x) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(x,REAL))
integral (((proj (r,n)) * f) || x) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * f) || x) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * f) || x) is non empty V13() V16( divs x) V17( REAL ) Function-like total V27( divs x, REAL ) V119() V120() V121() Element of K6(K7((divs x),REAL))
rng (upper_sum_set (((proj (r,n)) * f) || x)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * f) || x))) is V11() real ext-real Element of REAL
Z * (integral (((proj (r,n)) * f),x)) is V11() real ext-real Element of REAL
((proj (r,n)) * f) | x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
(proj (r,n)) * (f | x) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
dom ((proj (r,n)) * f) is V129() V130() V131() Element of K6(REAL)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(Z * (n,x,f)) . r is V11() real ext-real Element of REAL
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
(proj (r,n)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (r,n)) * f),x) is V11() real ext-real Element of REAL
((proj (r,n)) * f) || x is V13() V16(x) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(x,REAL))
K7(x,REAL) is V32() V119() V120() V121() set
K6(K7(x,REAL)) is V32() set
integral (((proj (r,n)) * f) || x) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * f) || x) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * f) || x) is non empty V13() V16( divs x) V17( REAL ) Function-like total V27( divs x, REAL ) V119() V120() V121() Element of K6(K7((divs x),REAL))
divs x is non empty set
K7((divs x),REAL) is V32() V119() V120() V121() set
K6(K7((divs x),REAL)) is V32() set
rng (upper_sum_set (((proj (r,n)) * f) || x)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * f) || x))) is V11() real ext-real Element of REAL
Z * (integral (((proj (r,n)) * f),x)) is V11() real ext-real Element of REAL
(n,x,f) . r is V11() real ext-real Element of REAL
Z * ((n,x,f) . r) is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,x,(n,Z,REAL,f)) . r is V11() real ext-real Element of REAL
(Z * (n,x,f)) . r is V11() real ext-real Element of REAL
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
(proj (r,n)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
Z (#) ((proj (r,n)) * f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral ((Z (#) ((proj (r,n)) * f)),x) is V11() real ext-real Element of REAL
(Z (#) ((proj (r,n)) * f)) || x is V13() V16(x) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(x,REAL))
K7(x,REAL) is V32() V119() V120() V121() set
K6(K7(x,REAL)) is V32() set
integral ((Z (#) ((proj (r,n)) * f)) || x) is V11() real ext-real Element of REAL
upper_integral ((Z (#) ((proj (r,n)) * f)) || x) is V11() real ext-real Element of REAL
upper_sum_set ((Z (#) ((proj (r,n)) * f)) || x) is non empty V13() V16( divs x) V17( REAL ) Function-like total V27( divs x, REAL ) V119() V120() V121() Element of K6(K7((divs x),REAL))
divs x is non empty set
K7((divs x),REAL) is V32() V119() V120() V121() set
K6(K7((divs x),REAL)) is V32() set
rng (upper_sum_set ((Z (#) ((proj (r,n)) * f)) || x)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((Z (#) ((proj (r,n)) * f)) || x))) is V11() real ext-real Element of REAL
(proj (r,n)) * (n,Z,REAL,f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (r,n)) * (n,Z,REAL,f)),x) is V11() real ext-real Element of REAL
((proj (r,n)) * (n,Z,REAL,f)) || x is V13() V16(x) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(x,REAL))
integral (((proj (r,n)) * (n,Z,REAL,f)) || x) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * (n,Z,REAL,f)) || x) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * (n,Z,REAL,f)) || x) is non empty V13() V16( divs x) V17( REAL ) Function-like total V27( divs x, REAL ) V119() V120() V121() Element of K6(K7((divs x),REAL))
rng (upper_sum_set (((proj (r,n)) * (n,Z,REAL,f)) || x)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * (n,Z,REAL,f)) || x))) is V11() real ext-real Element of REAL
integral (((proj (r,n)) * f),x) is V11() real ext-real Element of REAL
((proj (r,n)) * f) || x is V13() V16(x) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(x,REAL))
integral (((proj (r,n)) * f) || x) is V11() real ext-real Element of REAL
upper_integral (((proj (r,n)) * f) || x) is V11() real ext-real Element of REAL
upper_sum_set (((proj (r,n)) * f) || x) is non empty V13() V16( divs x) V17( REAL ) Function-like total V27( divs x, REAL ) V119() V120() V121() Element of K6(K7((divs x),REAL))
rng (upper_sum_set (((proj (r,n)) * f) || x)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (r,n)) * f) || x))) is V11() real ext-real Element of REAL
Z * (integral (((proj (r,n)) * f),x)) is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
proj (r,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
(proj (r,n)) * (n,Z,REAL,f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
(proj (r,n)) * f is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
((proj (r,n)) * f) | x is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
(proj (r,n)) * (f | x) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
dom ((proj (r,n)) * f) is V129() V130() V131() Element of K6(REAL)
Z (#) ((proj (r,n)) * f) is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
dom (n,x,(n,Z,REAL,f)) is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom (Z * (n,x,f)) is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is V32() set
K6(K7(REAL,(REAL n))) is V32() set
Z is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
x is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
(n,x,Z) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
f is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
[.f,r.] is V129() V130() V131() Element of K6(REAL)
(f,r,n,Z) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
dom (n,x,Z) is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
Seg n is V32() V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,x,Z) . k is V11() real ext-real Element of REAL
proj (k,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (k,n)) * Z is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (k,n)) * Z),x) is V11() real ext-real Element of REAL
((proj (k,n)) * Z) || x is V13() V16(x) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(x,REAL))
K7(x,REAL) is V32() V119() V120() V121() set
K6(K7(x,REAL)) is V32() set
integral (((proj (k,n)) * Z) || x) is V11() real ext-real Element of REAL
upper_integral (((proj (k,n)) * Z) || x) is V11() real ext-real Element of REAL
upper_sum_set (((proj (k,n)) * Z) || x) is non empty V13() V16( divs x) V17( REAL ) Function-like total V27( divs x, REAL ) V119() V120() V121() Element of K6(K7((divs x),REAL))
divs x is non empty set
K7((divs x),REAL) is V32() V119() V120() V121() set
K6(K7((divs x),REAL)) is V32() set
rng (upper_sum_set (((proj (k,n)) * Z) || x)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (k,n)) * Z) || x))) is V11() real ext-real Element of REAL
(f,r,n,Z) . k is V11() real ext-real Element of REAL
integral (((proj (k,n)) * Z),f,r) is V11() real ext-real Element of REAL
(n,x,Z) . i is V11() real ext-real Element of REAL
(f,r,n,Z) . i is V11() real ext-real Element of REAL
dom (f,r,n,Z) is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is V32() set
K6(K7(REAL,(REAL n))) is V32() set
Z is V13() V16( REAL ) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL n)))
x is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
(n,x,Z) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
- (n,x,Z) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
r is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
[.r,f.] is V129() V130() V131() Element of K6(REAL)
(f,r,n,Z) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
dom (- (n,x,Z)) is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom (n,x,Z) is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
Seg n is V32() V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(f,r,n,Z) . k is V11() real ext-real Element of REAL
proj (k,n) is non empty V13() V16( REAL n) V17( REAL ) Function-like total V27( REAL n, REAL ) V119() V120() V121() Element of K6(K7((REAL n),REAL))
K7((REAL n),REAL) is V32() V119() V120() V121() set
K6(K7((REAL n),REAL)) is V32() set
(proj (k,n)) * Z is V13() V16( REAL ) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(REAL,REAL))
integral (((proj (k,n)) * Z),f,r) is V11() real ext-real Element of REAL
(- (n,x,Z)) . k is V11() real ext-real Element of REAL
(n,x,Z) . k is V11() real ext-real Element of REAL
- ((n,x,Z) . k) is V11() real ext-real Element of REAL
integral (((proj (k,n)) * Z),x) is V11() real ext-real Element of REAL
((proj (k,n)) * Z) || x is V13() V16(x) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(x,REAL))
K7(x,REAL) is V32() V119() V120() V121() set
K6(K7(x,REAL)) is V32() set
integral (((proj (k,n)) * Z) || x) is V11() real ext-real Element of REAL
upper_integral (((proj (k,n)) * Z) || x) is V11() real ext-real Element of REAL
upper_sum_set (((proj (k,n)) * Z) || x) is non empty V13() V16( divs x) V17( REAL ) Function-like total V27( divs x, REAL ) V119() V120() V121() Element of K6(K7((divs x),REAL))
divs x is non empty set
K7((divs x),REAL) is V32() V119() V120() V121() set
K6(K7((divs x),REAL)) is V32() set
rng (upper_sum_set (((proj (k,n)) * Z) || x)) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((proj (k,n)) * Z) || x))) is V11() real ext-real Element of REAL
- (integral (((proj (k,n)) * Z),x)) is V11() real ext-real Element of REAL
(- (n,x,Z)) . i is V11() real ext-real Element of REAL
(f,r,n,Z) . i is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive Element of REAL
(- 1) (#) (n,x,Z) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() Element of K6(K7(NAT,REAL))
dom ((- 1) (#) (n,x,Z)) is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom (f,r,n,Z) is V39(n) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Z is set
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
x is set
f is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
r is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
(n,Z,f,r) is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
f <++> r is V13() V16(Z /\ Z) V17( R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((Z /\ Z),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))))
Z /\ Z is set
DOMS (REAL n) is set
(DOMS (REAL n)) /\ (DOMS (REAL n)) is set
R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K7((Z /\ Z),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))) is set
K6(K7((Z /\ Z),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))))) is set
dom (n,Z,f,r) is Element of K6(Z)
K6(Z) is set
(n,Z,f,r) /. x is V39(n) FinSequence-like V119() V120() V121() Element of REAL n
f /. x is V39(n) FinSequence-like V119() V120() V121() Element of REAL n
r /. x is V39(n) FinSequence-like V119() V120() V121() Element of REAL n
(f /. x) + (r /. x) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
dom f is Element of K6(Z)
dom r is Element of K6(Z)
(dom f) /\ (dom r) is Element of K6(Z)
f . x is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
r . x is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
(n,Z,f,r) . x is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Z is set
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
x is set
f is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
r is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
(n,Z,f,r) is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
f <--> r is V13() V16(Z /\ Z) V17( R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((Z /\ Z),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))))
Z /\ Z is set
DOMS (REAL n) is set
(DOMS (REAL n)) /\ (DOMS (REAL n)) is set
R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K7((Z /\ Z),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))) is set
K6(K7((Z /\ Z),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))))) is set
dom (n,Z,f,r) is Element of K6(Z)
K6(Z) is set
(n,Z,f,r) /. x is V39(n) FinSequence-like V119() V120() V121() Element of REAL n
f /. x is V39(n) FinSequence-like V119() V120() V121() Element of REAL n
r /. x is V39(n) FinSequence-like V119() V120() V121() Element of REAL n
(f /. x) - (r /. x) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
dom f is Element of K6(Z)
dom r is Element of K6(Z)
(dom f) /\ (dom r) is Element of K6(Z)
f . x is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
r . x is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
(n,Z,f,r) . x is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Z is set
K7(Z,(REAL n)) is set
K6(K7(Z,(REAL n))) is set
x is set
f is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
f /. x is V39(n) FinSequence-like V119() V120() V121() Element of REAL n
r is V11() real ext-real set
(n,r,Z,f) is V13() V16(Z) V17( REAL n) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(REAL n)))
f [#] r is V13() V16(Z) V17( R_PFuncs (DOMS (REAL n))) Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(Z,(R_PFuncs (DOMS (REAL n)))))
DOMS (REAL n) is set
R_PFuncs (DOMS (REAL n)) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K7(Z,(R_PFuncs (DOMS (REAL n)))) is set
K6(K7(Z,(R_PFuncs (DOMS (REAL n))))) is set
dom (n,r,Z,f) is Element of K6(Z)
K6(Z) is set
(n,r,Z,f) /. x is V39(n) FinSequence-like V119() V120() V121() Element of REAL n
r * (f /. x) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39(n) FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL n
dom f is Element of K6(Z)
f . x is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set
(n,r,Z,f) . x is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() set