:: MESFUNC4 semantic presentation

REAL is non empty V37() V85() V86() V87() V91() set
NAT is non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() Element of K19(REAL)
K19(REAL) is V37() set
ExtREAL is non empty V86() set
K20(NAT,ExtREAL) is V37() V62() set
K19(K20(NAT,ExtREAL)) is V37() set
K19(ExtREAL) is set
COMPLEX is non empty V37() V85() V91() set
NAT is non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() set
K19(NAT) is V37() set
K19(NAT) is V37() set
K20(NAT,REAL) is V37() V61() V62() V63() set
K19(K20(NAT,REAL)) is V37() set
K19(K19(REAL)) is V37() set
RAT is non empty V37() V85() V86() V87() V88() V91() set
K19(RAT) is V37() set
INT is non empty V37() V85() V86() V87() V88() V89() V91() set
K20(COMPLEX,COMPLEX) is V37() V61() set
K19(K20(COMPLEX,COMPLEX)) is V37() set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is V37() V61() set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V37() set
K20(REAL,REAL) is V37() V61() V62() V63() set
K19(K20(REAL,REAL)) is V37() set
K20(K20(REAL,REAL),REAL) is V37() V61() V62() V63() set
K19(K20(K20(REAL,REAL),REAL)) is V37() set
K20(RAT,RAT) is RAT -valued V37() V61() V62() V63() set
K19(K20(RAT,RAT)) is V37() set
K20(K20(RAT,RAT),RAT) is RAT -valued V37() V61() V62() V63() set
K19(K20(K20(RAT,RAT),RAT)) is V37() set
K20(INT,INT) is RAT -valued INT -valued V37() V61() V62() V63() set
K19(K20(INT,INT)) is V37() set
K20(K20(INT,INT),INT) is RAT -valued INT -valued V37() V61() V62() V63() set
K19(K20(K20(INT,INT),INT)) is V37() set
K20(NAT,NAT) is RAT -valued INT -valued V37() V61() V62() V63() V64() set
K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued V37() V61() V62() V63() V64() set
K19(K20(K20(NAT,NAT),NAT)) is V37() set
K351() is set
1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
{} is set
the Function-like functional empty V15() V16() V17() V19() V20() V21() V22() V23() ext-real non positive non negative V37() V42() V44( {} ) FinSequence-membered V85() V86() V87() V88() V89() V90() V91() set is Function-like functional empty V15() V16() V17() V19() V20() V21() V22() V23() ext-real non positive non negative V37() V42() V44( {} ) FinSequence-membered V85() V86() V87() V88() V89() V90() V91() set
{{},1} is set
2 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
3 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
0 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
-infty is non empty V23() ext-real non positive negative Element of ExtREAL
{-infty} is non empty V12() V44(1) V86() set
+infty is non empty V23() ext-real positive non negative Element of ExtREAL
{+infty} is non empty V12() V44(1) V86() set
1. is ext-real Element of ExtREAL
union {} is set
Seg 1 is non empty V12() V37() V44(1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
{1} is non empty V12() V44(1) V85() V86() V87() V88() V89() V90() set
Seg 2 is non empty V37() V44(2) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
{1,2} is V85() V86() V87() V88() V89() V90() set
dom {} is set
rng {} is set
0. is ext-real Element of ExtREAL
+infty is non empty V23() ext-real positive non negative set
-infty is non empty V23() ext-real non positive negative set
X is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom X is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
S is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom S is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
M is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
X + S is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
Sum M is ext-real Element of ExtREAL
Sum X is ext-real Element of ExtREAL
Sum S is ext-real Element of ExtREAL
(Sum X) + (Sum S) is ext-real Element of ExtREAL
rng X is V86() set
f is set
g is set
X . g is ext-real Element of ExtREAL
c is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
X . c is ext-real Element of ExtREAL
X " {-infty} is set
rng S is V86() set
f is set
g is set
S . g is ext-real Element of ExtREAL
c is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
S . c is ext-real Element of ExtREAL
S " {-infty} is set
dom M is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
(dom X) /\ (dom S) is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
S " {+infty} is set
(X " {-infty}) /\ (S " {+infty}) is set
X " {+infty} is set
(X " {+infty}) /\ (S " {-infty}) is set
((X " {-infty}) /\ (S " {+infty})) \/ ((X " {+infty}) /\ (S " {-infty})) is set
((dom X) /\ (dom S)) \ (((X " {-infty}) /\ (S " {+infty})) \/ ((X " {+infty}) /\ (S " {-infty}))) is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
len M is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
len X is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
f is Relation-like NAT -defined ExtREAL -valued Function-like V30( NAT , ExtREAL ) V62() Element of K19(K20(NAT,ExtREAL))
f . (len M) is ext-real Element of ExtREAL
f . 0 is ext-real Element of ExtREAL
g is Relation-like NAT -defined ExtREAL -valued Function-like V30( NAT , ExtREAL ) V62() Element of K19(K20(NAT,ExtREAL))
g . (len X) is ext-real Element of ExtREAL
g . 0 is ext-real Element of ExtREAL
len S is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
c is Relation-like NAT -defined ExtREAL -valued Function-like V30( NAT , ExtREAL ) V62() Element of K19(K20(NAT,ExtREAL))
c . (len S) is ext-real Element of ExtREAL
c . 0 is ext-real Element of ExtREAL
F is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
f . F is ext-real Element of ExtREAL
g . F is ext-real Element of ExtREAL
c . F is ext-real Element of ExtREAL
(g . F) + (c . F) is ext-real Element of ExtREAL
F + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
f . (F + 1) is ext-real Element of ExtREAL
g . (F + 1) is ext-real Element of ExtREAL
c . (F + 1) is ext-real Element of ExtREAL
(g . (F + 1)) + (c . (F + 1)) is ext-real Element of ExtREAL
a is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
a + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
g . (a + 1) is ext-real Element of ExtREAL
g . a is ext-real Element of ExtREAL
X . (a + 1) is ext-real Element of ExtREAL
(g . a) + (X . (a + 1)) is ext-real Element of ExtREAL
c . (a + 1) is ext-real Element of ExtREAL
c . a is ext-real Element of ExtREAL
S . (a + 1) is ext-real Element of ExtREAL
(c . a) + (S . (a + 1)) is ext-real Element of ExtREAL
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
g . x is ext-real Element of ExtREAL
x + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
g . (x + 1) is ext-real Element of ExtREAL
b is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
b + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
X . (b + 1) is ext-real Element of ExtREAL
g . (b + 1) is ext-real Element of ExtREAL
g . b is ext-real Element of ExtREAL
(g . b) + (X . (b + 1)) is ext-real Element of ExtREAL
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
c . x is ext-real Element of ExtREAL
x + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
c . (x + 1) is ext-real Element of ExtREAL
b is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
b + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
S . (b + 1) is ext-real Element of ExtREAL
c . (b + 1) is ext-real Element of ExtREAL
c . b is ext-real Element of ExtREAL
(c . b) + (S . (b + 1)) is ext-real Element of ExtREAL
f . (a + 1) is ext-real Element of ExtREAL
(g . a) + (c . a) is ext-real Element of ExtREAL
M . (a + 1) is ext-real Element of ExtREAL
((g . a) + (c . a)) + (M . (a + 1)) is ext-real Element of ExtREAL
(X . (a + 1)) + (S . (a + 1)) is ext-real Element of ExtREAL
((g . a) + (c . a)) + ((X . (a + 1)) + (S . (a + 1))) is ext-real Element of ExtREAL
((g . a) + (c . a)) + (X . (a + 1)) is ext-real Element of ExtREAL
(((g . a) + (c . a)) + (X . (a + 1))) + (S . (a + 1)) is ext-real Element of ExtREAL
((g . a) + (X . (a + 1))) + (c . a) is ext-real Element of ExtREAL
(((g . a) + (X . (a + 1))) + (c . a)) + (S . (a + 1)) is ext-real Element of ExtREAL
(g . (a + 1)) + (c . (a + 1)) is ext-real Element of ExtREAL
(g . 0) + (c . 0) is ext-real Element of ExtREAL
X is non empty set
K19(X) is set
K19(K19(X)) is set
K20(X,ExtREAL) is V62() set
K19(K20(X,ExtREAL)) is set
S is non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive Element of K19(K19(X))
K20(S,ExtREAL) is V62() set
K19(K20(S,ExtREAL)) is set
M is Relation-like S -defined ExtREAL -valued Function-like V30(S, ExtREAL ) V62() V70() nonnegative sigma-additive Element of K19(K20(S,ExtREAL))
f is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
f + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
g is Relation-like X -defined ExtREAL -valued Function-like V62() Element of K19(K20(X,ExtREAL))
dom g is set
integral (X,S,M,g) is ext-real Element of ExtREAL
c is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
dom c is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
M * c is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
len c is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
F is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
a is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom a is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Sum a is ext-real Element of ExtREAL
x is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg x is V37() V44(x) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
c | (Seg x) is Relation-like NAT -defined S -valued Function-like FinSubsequence-like Element of K19(K20(NAT,S))
K20(NAT,S) is V37() set
K19(K20(NAT,S)) is V37() set
rng (c | (Seg x)) is set
union (rng (c | (Seg x))) is set
g | (union (rng (c | (Seg x)))) is Relation-like X -defined ExtREAL -valued Function-like V62() Element of K19(K20(X,ExtREAL))
dom (g | (union (rng (c | (Seg x))))) is set
x is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
rng x is set
union (rng x) is set
(dom g) /\ (union (rng x)) is set
rng c is set
union (rng c) is set
(union (rng c)) /\ (union (rng x)) is set
x is set
(g | (union (rng (c | (Seg x))))) . x is ext-real Element of ExtREAL
g . x is ext-real Element of ExtREAL
F | (Seg x) is Relation-like NAT -defined ExtREAL -valued Function-like FinSubsequence-like V62() Element of K19(K20(NAT,ExtREAL))
a | (Seg x) is Relation-like NAT -defined ExtREAL -valued Function-like FinSubsequence-like V62() Element of K19(K20(NAT,ExtREAL))
FG is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom FG is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
(dom c) /\ (Seg x) is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
dom x is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
a1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x . a1 is set
b1 is Element of X
y1 is Element of X
(g | (union (rng (c | (Seg x))))) . b1 is ext-real Element of ExtREAL
(g | (union (rng (c | (Seg x))))) . y1 is ext-real Element of ExtREAL
g . b1 is ext-real Element of ExtREAL
g . y1 is ext-real Element of ExtREAL
c . a1 is set
F . a1 is ext-real Element of ExtREAL
a1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
b1 is Element of X
x . a1 is set
y1 is Element of X
(g | (union (rng (c | (Seg x))))) . b1 is ext-real Element of ExtREAL
(g | (union (rng (c | (Seg x))))) . y1 is ext-real Element of ExtREAL
a1 is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
rng a1 is set
union (rng a1) is set
dom a1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
dom F is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
(dom F) /\ (Seg x) is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
k is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom k is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
a1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x . a1 is set
k . a1 is ext-real Element of ExtREAL
c . a1 is set
F . a1 is ext-real Element of ExtREAL
b1 is set
(g | (union (rng (c | (Seg x))))) . b1 is ext-real Element of ExtREAL
g . b1 is ext-real Element of ExtREAL
x + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
c . (x + 1) is set
(union (rng x)) \/ (c . (x + 1)) is set
a1 is set
b1 is set
y1 is set
c . y1 is set
x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg (len c) is V37() V44( len c) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x . x1 is set
a1 is set
b1 is set
y1 is set
x . y1 is set
c . y1 is set
len a is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg (len a) is V37() V44( len a) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Seg (x + 1) is non empty V37() V44(x + 1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
a1 is Relation-like NAT -defined ExtREAL -valued Function-like V30( NAT , ExtREAL ) V62() Element of K19(K20(NAT,ExtREAL))
a1 . (len a) is ext-real Element of ExtREAL
a1 . 0 is ext-real Element of ExtREAL
b1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x . b1 is set
y1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
a . y1 is ext-real Element of ExtREAL
x . y1 is set
c . y1 is set
F . y1 is ext-real Element of ExtREAL
(M * c) . y1 is ext-real Element of ExtREAL
(F . y1) * ((M * c) . y1) is ext-real Element of ExtREAL
b1 is Element of S
M . b1 is ext-real Element of ExtREAL
b1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
a1 . b1 is ext-real Element of ExtREAL
b1 + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
a1 . (b1 + 1) is ext-real Element of ExtREAL
a . (b1 + 1) is ext-real Element of ExtREAL
0. + (a . (b1 + 1)) is ext-real Element of ExtREAL
a1 . (x + 1) is ext-real Element of ExtREAL
a1 . x is ext-real Element of ExtREAL
a . (x + 1) is ext-real Element of ExtREAL
(a1 . x) + (a . (x + 1)) is ext-real Element of ExtREAL
0. + (a . (x + 1)) is ext-real Element of ExtREAL
F . (x + 1) is ext-real Element of ExtREAL
b1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x1 is ext-real Element of ExtREAL
x1 is ext-real Element of ExtREAL
b1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom b1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
y1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
c1 is Element of S
c1 is Element of S
y1 is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of S
dom y1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
b1 . 1 is ext-real Element of ExtREAL
b1 . 2 is ext-real Element of ExtREAL
y1 . 2 is set
y1 . 1 is set
x1 is set
c1 is set
y1 . x1 is set
y1 . c1 is set
z1 is set
x is set
lb9 is set
x . lb9 is set
k is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
c . k is set
z1 is set
x is set
lb9 is set
x . lb9 is set
k is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
c . k is set
len y1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
<*(union (rng x)),(c . (x + 1))*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
M * y1 is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
x1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
len x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
dom x1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x1 . 1 is ext-real Element of ExtREAL
(M * y1) . 1 is ext-real Element of ExtREAL
(b1 . 1) * ((M * y1) . 1) is ext-real Element of ExtREAL
Sum x1 is ext-real Element of ExtREAL
c1 is Relation-like NAT -defined ExtREAL -valued Function-like V30( NAT , ExtREAL ) V62() Element of K19(K20(NAT,ExtREAL))
c1 . (len x1) is ext-real Element of ExtREAL
c1 . 0 is ext-real Element of ExtREAL
c1 . 1 is ext-real Element of ExtREAL
0 + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
x1 . (0 + 1) is ext-real Element of ExtREAL
(c1 . 0) + (x1 . (0 + 1)) is ext-real Element of ExtREAL
(M * y1) . 2 is ext-real Element of ExtREAL
M . (c . (x + 1)) is ext-real Element of ExtREAL
(M * c) . (x + 1) is ext-real Element of ExtREAL
x1 . 2 is ext-real Element of ExtREAL
(F . (x + 1)) * ((M * c) . (x + 1)) is ext-real Element of ExtREAL
z1 is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
dom z1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
z1 . x is set
b1 . x is ext-real Element of ExtREAL
lb9 is set
g . lb9 is ext-real Element of ExtREAL
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
b1 . x is ext-real Element of ExtREAL
z1 . x is set
lb9 is set
g . lb9 is ext-real Element of ExtREAL
k is Element of X
g . k is ext-real Element of ExtREAL
|.(g . k).| is ext-real Element of ExtREAL
{(union (rng x)),(c . (x + 1))} is set
union {(union (rng x)),(c . (x + 1))} is set
rng z1 is set
union (rng z1) is set
1 + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
c1 . (1 + 1) is ext-real Element of ExtREAL
F . (x + 1) is ext-real Element of ExtREAL
b1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x1 is Element of S
y1 is Element of S
b1 is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of S
dom b1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
y1 is set
x1 is set
b1 . y1 is set
b1 . x1 is set
y1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
c1 is ext-real Element of ExtREAL
c1 is ext-real Element of ExtREAL
y1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom y1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
b1 . 2 is set
M . (b1 . 2) is ext-real Element of ExtREAL
M * b1 is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
(M * b1) . 2 is ext-real Element of ExtREAL
b1 . 1 is set
y1 . 1 is ext-real Element of ExtREAL
x1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
len x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
dom x1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x1 . 2 is ext-real Element of ExtREAL
y1 . 2 is ext-real Element of ExtREAL
(y1 . 2) * ((M * b1) . 2) is ext-real Element of ExtREAL
x1 . 1 is ext-real Element of ExtREAL
(M * b1) . 1 is ext-real Element of ExtREAL
(y1 . 1) * ((M * b1) . 1) is ext-real Element of ExtREAL
c1 is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
dom c1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
z1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
c1 . z1 is set
y1 . z1 is ext-real Element of ExtREAL
x is set
g . x is ext-real Element of ExtREAL
len c1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
<*(union (rng c)),{}*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
rng c1 is set
{(union (rng c)),{}} is set
union (rng c1) is set
(union (rng c)) \/ {} is set
Sum x1 is ext-real Element of ExtREAL
z1 is Relation-like NAT -defined ExtREAL -valued Function-like V30( NAT , ExtREAL ) V62() Element of K19(K20(NAT,ExtREAL))
z1 . (len x1) is ext-real Element of ExtREAL
z1 . 0 is ext-real Element of ExtREAL
z1 . 1 is ext-real Element of ExtREAL
0 + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
x1 . (0 + 1) is ext-real Element of ExtREAL
(z1 . 0) + (x1 . (0 + 1)) is ext-real Element of ExtREAL
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
y1 . x is ext-real Element of ExtREAL
(M * c) . (x + 1) is ext-real Element of ExtREAL
(F . (x + 1)) * ((M * c) . (x + 1)) is ext-real Element of ExtREAL
1 + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
x1 . (1 + 1) is ext-real Element of ExtREAL
(z1 . 1) + (x1 . (1 + 1)) is ext-real Element of ExtREAL
F . (x + 1) is ext-real Element of ExtREAL
F . (x + 1) is ext-real Element of ExtREAL
x + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg (x + 1) is non empty V37() V44(x + 1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
(Seg (x + 1)) /\ (Seg x) is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
len x is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
integral (X,S,M,(g | (union (rng (c | (Seg x)))))) is ext-real Element of ExtREAL
a1 is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
b1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
b1 . 1 is ext-real Element of ExtREAL
dom b1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
y1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom y1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
dom a1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
M * a1 is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
Sum y1 is ext-real Element of ExtREAL
M * x is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
FG . x1 is ext-real Element of ExtREAL
k . x1 is ext-real Element of ExtREAL
(M * x) . x1 is ext-real Element of ExtREAL
(k . x1) * ((M * x) . x1) is ext-real Element of ExtREAL
a . x1 is ext-real Element of ExtREAL
F . x1 is ext-real Element of ExtREAL
(M * c) . x1 is ext-real Element of ExtREAL
(F . x1) * ((M * c) . x1) is ext-real Element of ExtREAL
(k . x1) * ((M * c) . x1) is ext-real Element of ExtREAL
c . x1 is set
M . (c . x1) is ext-real Element of ExtREAL
x . x1 is set
M . (x . x1) is ext-real Element of ExtREAL
c . (x + 1) is set
F . (x + 1) is ext-real Element of ExtREAL
a1 . 1 is set
(a1 . 1) \/ (c . (x + 1)) is set
len a1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg (len a1) is V37() V44( len a1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
a1 . x1 is set
rng a1 is set
z1 is Element of S
z1 is Element of S
x1 is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of S
dom x1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
c1 is set
z1 is set
x1 . c1 is set
x1 . z1 is set
lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
1 + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
a1 . z1 is set
k is set
a1 . lb9 is set
rng a1 is set
union (rng a1) is set
g . k is ext-real Element of ExtREAL
(g | (union (rng (c | (Seg x))))) . k is ext-real Element of ExtREAL
b1 . lb9 is ext-real Element of ExtREAL
x is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
1 + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
a1 . c1 is set
k is set
a1 . x is set
rng a1 is set
union (rng a1) is set
g . k is ext-real Element of ExtREAL
(g | (union (rng (c | (Seg x))))) . k is ext-real Element of ExtREAL
b1 . x is ext-real Element of ExtREAL
lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
a1 . z1 is set
M * x1 is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
len y1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
z1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
len z1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
dom z1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
0 + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
c1 is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
rng c1 is set
union (rng c1) is set
x is set
lb9 is set
k is set
c . k is set
p is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg (len c) is V37() V44( len c) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
c1 . 1 is set
(a1 . 1) \/ lb9 is set
x . p is set
rng a1 is set
union (rng a1) is set
q is set
v is set
a1 . v is set
EMPTY is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
c1 . 1 is set
1 + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
c1 . EMPTY is set
x is set
lb9 is set
dom c1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
k is set
c1 . k is set
p is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
c1 . p is set
rng a1 is set
union (rng a1) is set
p is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
1 + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
a1 . p is set
rng a1 is set
union (rng a1) is set
p is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
rng FG is V86() set
x is set
FG . x is ext-real Element of ExtREAL
lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(dom a) /\ (Seg x) is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
a . lb9 is ext-real Element of ExtREAL
F . lb9 is ext-real Element of ExtREAL
(M * c) . lb9 is ext-real Element of ExtREAL
(F . lb9) * ((M * c) . lb9) is ext-real Element of ExtREAL
c . lb9 is set
p is set
k is Element of S
M . {} is ext-real Element of ExtREAL
q is Element of S
M . q is ext-real Element of ExtREAL
g . p is ext-real Element of ExtREAL
c . lb9 is set
M . (c . lb9) is ext-real Element of ExtREAL
c . lb9 is set
a . (x + 1) is ext-real Element of ExtREAL
(M * c) . (x + 1) is ext-real Element of ExtREAL
M . (c . (x + 1)) is ext-real Element of ExtREAL
(F . (x + 1)) * ((M * c) . (x + 1)) is ext-real Element of ExtREAL
(M * c) . (x + 1) is ext-real Element of ExtREAL
(F . (x + 1)) * ((M * c) . (x + 1)) is ext-real Element of ExtREAL
<*(a . (x + 1))*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V37() V44(1) FinSequence-like FinSubsequence-like V62() V65() V66() V67() V68() FinSequence of ExtREAL
rng <*(a . (x + 1))*> is V12() V86() set
{(a . (x + 1))} is non empty V12() V44(1) V86() set
dom c1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
c1 . x is set
b1 . x is ext-real Element of ExtREAL
lb9 is set
g . lb9 is ext-real Element of ExtREAL
rng a1 is set
union (rng a1) is set
(g | (union (rng (c | (Seg x))))) . lb9 is ext-real Element of ExtREAL
1 + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
a1 . x is set
rng a1 is set
union (rng a1) is set
(g | (union (rng (c | (Seg x))))) . lb9 is ext-real Element of ExtREAL
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
z1 . x is ext-real Element of ExtREAL
y1 . x is ext-real Element of ExtREAL
b1 . x is ext-real Element of ExtREAL
M * c1 is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
(M * c1) . x is ext-real Element of ExtREAL
(b1 . x) * ((M * c1) . x) is ext-real Element of ExtREAL
(M * a1) . x is ext-real Element of ExtREAL
(b1 . x) * ((M * a1) . x) is ext-real Element of ExtREAL
1 + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
c1 . x is set
M . (c1 . x) is ext-real Element of ExtREAL
a1 . x is set
M . (a1 . x) is ext-real Element of ExtREAL
len a is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
a | (x + 1) is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
a | (Seg (x + 1)) is Relation-like NAT -defined ExtREAL -valued Function-like FinSubsequence-like V62() Element of K19(K20(NAT,ExtREAL))
FG ^ <*(a . (x + 1))*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
Sum FG is ext-real Element of ExtREAL
Sum <*(a . (x + 1))*> is ext-real Element of ExtREAL
(Sum FG) + (Sum <*(a . (x + 1))*>) is ext-real Element of ExtREAL
(Sum FG) + 0. is ext-real Element of ExtREAL
Sum z1 is ext-real Element of ExtREAL
c . (x + 1) is set
F . (x + 1) is ext-real Element of ExtREAL
len b1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(len b1) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
x1 is set
Seg ((len b1) + 1) is non empty V37() V44((len b1) + 1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
c1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
b1 . c1 is ext-real Element of ExtREAL
z1 is ext-real Element of ExtREAL
z1 is ext-real Element of ExtREAL
c1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom c1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
z1 is Element of X
g . z1 is ext-real Element of ExtREAL
|.(F . (x + 1)).| is ext-real Element of ExtREAL
len c1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
c1 . x is ext-real Element of ExtREAL
b1 . x is ext-real Element of ExtREAL
rng y1 is V86() set
(M * c) . (x + 1) is ext-real Element of ExtREAL
(F . (x + 1)) * ((M * c) . (x + 1)) is ext-real Element of ExtREAL
<*((F . (x + 1)) * ((M * c) . (x + 1)))*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V37() V44(1) FinSequence-like FinSubsequence-like V62() V65() V66() V67() V68() FinSequence of ExtREAL
rng <*((F . (x + 1)) * ((M * c) . (x + 1)))*> is V12() V86() set
x is set
y1 . x is ext-real Element of ExtREAL
lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
y1 . lb9 is ext-real Element of ExtREAL
b1 . lb9 is ext-real Element of ExtREAL
(M * a1) . lb9 is ext-real Element of ExtREAL
(b1 . lb9) * ((M * a1) . lb9) is ext-real Element of ExtREAL
len y1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg (len y1) is V37() V44( len y1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
1 + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
a1 . lb9 is set
rng a1 is set
p is Element of S
M . p is ext-real Element of ExtREAL
k is Element of S
M . k is ext-real Element of ExtREAL
M . (a1 . lb9) is ext-real Element of ExtREAL
lb9 is Element of S
M . lb9 is ext-real Element of ExtREAL
x is Element of S
M . x is ext-real Element of ExtREAL
{((F . (x + 1)) * ((M * c) . (x + 1)))} is non empty V12() V44(1) V86() set
rng FG is V86() set
lb9 is set
FG . lb9 is ext-real Element of ExtREAL
k is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(dom a) /\ (Seg x) is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
a . k is ext-real Element of ExtREAL
F . k is ext-real Element of ExtREAL
(M * c) . k is ext-real Element of ExtREAL
(F . k) * ((M * c) . k) is ext-real Element of ExtREAL
c . k is set
q is set
g . q is ext-real Element of ExtREAL
x is Element of S
M . x is ext-real Element of ExtREAL
p is Element of S
M . p is ext-real Element of ExtREAL
M . (c . k) is ext-real Element of ExtREAL
len a1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(len a1) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg (len a1) is V37() V44( len a1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Seg (len b1) is V37() V44( len b1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Seg ((len a1) + 1) is non empty V37() V44((len a1) + 1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
a1 . x is set
rng a1 is set
lb9 is Element of S
lb9 is Element of S
x is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of S
dom x is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
lb9 is set
k is set
x . lb9 is set
x . k is set
p is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
q is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
v is set
EMPTY is set
m is set
x . m is set
m is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg (len x) is V37() V44( len x) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x . m is set
c . m is set
EMPTY /\ (c . (x + 1)) is set
v is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x . v is set
a1 . v is set
rng a1 is set
union (rng a1) is set
x . p is set
a1 . p is set
x . q is set
a1 . q is set
len x is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg (len x) is V37() V44( len x) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
len y1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
M * x is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
(len y1) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg ((len y1) + 1) is non empty V37() V44((len y1) + 1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
b1 . lb9 is ext-real Element of ExtREAL
(M * x) . lb9 is ext-real Element of ExtREAL
(b1 . lb9) * ((M * x) . lb9) is ext-real Element of ExtREAL
k is ext-real Element of ExtREAL
k is ext-real Element of ExtREAL
lb9 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom lb9 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
len lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
M . (c . (x + 1)) is ext-real Element of ExtREAL
x . (len lb9) is set
M . (x . (len lb9)) is ext-real Element of ExtREAL
(M * x) . (len lb9) is ext-real Element of ExtREAL
k is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
lb9 . k is ext-real Element of ExtREAL
c1 . k is ext-real Element of ExtREAL
(M * x) . k is ext-real Element of ExtREAL
(c1 . k) * ((M * x) . k) is ext-real Element of ExtREAL
b1 . k is ext-real Element of ExtREAL
lb9 . (len lb9) is ext-real Element of ExtREAL
y1 ^ <*((F . (x + 1)) * ((M * c) . (x + 1)))*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
p is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
lb9 . p is ext-real Element of ExtREAL
(y1 ^ <*((F . (x + 1)) * ((M * c) . (x + 1)))*>) . p is ext-real Element of ExtREAL
y1 . p is ext-real Element of ExtREAL
b1 . p is ext-real Element of ExtREAL
(M * a1) . p is ext-real Element of ExtREAL
(b1 . p) * ((M * a1) . p) is ext-real Element of ExtREAL
a1 . p is set
M . (a1 . p) is ext-real Element of ExtREAL
(b1 . p) * (M . (a1 . p)) is ext-real Element of ExtREAL
Seg (len lb9) is V37() V44( len lb9) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
k is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
k . p is set
M . (k . p) is ext-real Element of ExtREAL
M * k is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
(M * k) . p is ext-real Element of ExtREAL
len (y1 ^ <*((F . (x + 1)) * ((M * c) . (x + 1)))*>) is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
len a is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
a | (x + 1) is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
a | (Seg (x + 1)) is Relation-like NAT -defined ExtREAL -valued Function-like FinSubsequence-like V62() Element of K19(K20(NAT,ExtREAL))
a . (x + 1) is ext-real Element of ExtREAL
<*(a . (x + 1))*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V37() V44(1) FinSequence-like FinSubsequence-like V62() V65() V66() V67() V68() FinSequence of ExtREAL
FG ^ <*(a . (x + 1))*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
FG ^ <*((F . (x + 1)) * ((M * c) . (x + 1)))*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
rng a1 is set
union (rng a1) is set
k is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
len k is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
<*(c . (x + 1))*> is Relation-like NAT -defined Function-like constant non empty V12() V37() V44(1) FinSequence-like FinSubsequence-like set
a1 ^ <*(c . (x + 1))*> is Relation-like NAT -defined Function-like non empty V37() FinSequence-like FinSubsequence-like set
p is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
k . p is set
(a1 ^ <*(c . (x + 1))*>) . p is set
a1 . p is set
len <*(c . (x + 1))*> is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(len a1) + (len <*(c . (x + 1))*>) is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
len (a1 ^ <*(c . (x + 1))*>) is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
rng k is set
rng a1 is set
rng <*(c . (x + 1))*> is V12() set
(rng a1) \/ (rng <*(c . (x + 1))*>) is set
{(c . (x + 1))} is non empty V12() V44(1) set
(rng a1) \/ {(c . (x + 1))} is set
c | (Seg (x + 1)) is Relation-like NAT -defined S -valued Function-like FinSubsequence-like Element of K19(K20(NAT,S))
x ^ <*(c . (x + 1))*> is Relation-like NAT -defined Function-like non empty V37() FinSequence-like FinSubsequence-like set
c | (x + 1) is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of S
(rng x) \/ (rng <*(c . (x + 1))*>) is set
(rng x) \/ {(c . (x + 1))} is set
union ((rng x) \/ {(c . (x + 1))}) is set
union {(c . (x + 1))} is set
(dom (g | (union (rng (c | (Seg x)))))) \/ (union {(c . (x + 1))}) is set
union (rng a1) is set
(union (rng a1)) \/ (union {(c . (x + 1))}) is set
union (rng k) is set
dom k is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
p is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
k . p is set
c1 . p is ext-real Element of ExtREAL
a1 . p is set
q is set
g . q is ext-real Element of ExtREAL
b1 . p is ext-real Element of ExtREAL
(g | (union (rng (c | (Seg x))))) . q is ext-real Element of ExtREAL
c1 . 1 is ext-real Element of ExtREAL
Sum lb9 is ext-real Element of ExtREAL
M * k is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
(M * k) . (len lb9) is ext-real Element of ExtREAL
(F . (x + 1)) * ((M * k) . (len lb9)) is ext-real Element of ExtREAL
<*((F . (x + 1)) * ((M * k) . (len lb9)))*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V37() V44(1) FinSequence-like FinSubsequence-like V62() V65() V66() V67() V68() FinSequence of ExtREAL
Sum <*((F . (x + 1)) * ((M * k) . (len lb9)))*> is ext-real Element of ExtREAL
(Sum y1) + (Sum <*((F . (x + 1)) * ((M * k) . (len lb9)))*>) is ext-real Element of ExtREAL
(integral (X,S,M,(g | (union (rng (c | (Seg x))))))) + ((F . (x + 1)) * ((M * k) . (len lb9))) is ext-real Element of ExtREAL
Sum FG is ext-real Element of ExtREAL
(Sum FG) + ((F . (x + 1)) * ((M * c) . (x + 1))) is ext-real Element of ExtREAL
Sum <*((F . (x + 1)) * ((M * c) . (x + 1)))*> is ext-real Element of ExtREAL
(Sum FG) + (Sum <*((F . (x + 1)) * ((M * c) . (x + 1)))*>) is ext-real Element of ExtREAL
c . (x + 1) is set
F . (x + 1) is ext-real Element of ExtREAL
c . (x + 1) is set
F . (x + 1) is ext-real Element of ExtREAL
f is Relation-like X -defined ExtREAL -valued Function-like V62() Element of K19(K20(X,ExtREAL))
dom f is set
integral (X,S,M,f) is ext-real Element of ExtREAL
g is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
dom g is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
M * g is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
len g is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
c is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
F is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom F is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Sum F is ext-real Element of ExtREAL
Seg (len g) is V37() V44( len g) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
rng g is set
union (rng g) is set
g is Relation-like X -defined ExtREAL -valued Function-like V62() Element of K19(K20(X,ExtREAL))
dom g is set
c is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
F is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
a is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom a is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
dom c is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
M * c is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
len c is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
f is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
integral (X,S,M,g) is ext-real Element of ExtREAL
Sum a is ext-real Element of ExtREAL
X is non empty set
K19(X) is set
K19(K19(X)) is set
K20(X,ExtREAL) is V62() set
K19(K20(X,ExtREAL)) is set
S is non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive Element of K19(K19(X))
K20(S,ExtREAL) is V62() set
K19(K20(S,ExtREAL)) is set
M is Relation-like X -defined ExtREAL -valued Function-like V62() Element of K19(K20(X,ExtREAL))
dom M is set
f is Relation-like S -defined ExtREAL -valued Function-like V30(S, ExtREAL ) V62() V70() nonnegative sigma-additive Element of K19(K20(S,ExtREAL))
integral (X,S,f,M) is ext-real Element of ExtREAL
g is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
dom g is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
f * g is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
c is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
F is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom F is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Sum F is ext-real Element of ExtREAL
len g is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
X is non empty set
K19(X) is set
K19(K19(X)) is set
K20(X,ExtREAL) is V62() set
K19(K20(X,ExtREAL)) is set
S is non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive Element of K19(K19(X))
K20(S,ExtREAL) is V62() set
K19(K20(S,ExtREAL)) is set
M is Relation-like X -defined ExtREAL -valued Function-like V62() Element of K19(K20(X,ExtREAL))
dom M is set
f is Relation-like S -defined ExtREAL -valued Function-like V30(S, ExtREAL ) V62() V70() nonnegative sigma-additive Element of K19(K20(S,ExtREAL))
integral (X,S,f,M) is ext-real Element of ExtREAL
g is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
c is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom g is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
f * g is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
len g is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
F is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
len F is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
dom F is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Seg (len g) is V37() V44( len g) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
a is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
F . a is ext-real Element of ExtREAL
c . a is ext-real Element of ExtREAL
(f * g) . a is ext-real Element of ExtREAL
(c . a) * ((f * g) . a) is ext-real Element of ExtREAL
F is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom F is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
F is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom F is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Sum F is ext-real Element of ExtREAL
X is non empty set
K19(X) is set
K19(K19(X)) is set
K20(X,ExtREAL) is V62() set
K19(K20(X,ExtREAL)) is set
S is non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive Element of K19(K19(X))
K20(S,ExtREAL) is V62() set
K19(K20(S,ExtREAL)) is set
M is Relation-like S -defined ExtREAL -valued Function-like V30(S, ExtREAL ) V62() V70() nonnegative sigma-additive Element of K19(K20(S,ExtREAL))
f is Relation-like X -defined ExtREAL -valued Function-like V62() Element of K19(K20(X,ExtREAL))
dom f is set
g is Relation-like X -defined ExtREAL -valued Function-like V62() Element of K19(K20(X,ExtREAL))
dom g is set
f + g is Relation-like X -defined ExtREAL -valued Function-like V62() Element of K19(K20(X,ExtREAL))
dom (f + g) is set
integral (X,S,M,(f + g)) is ext-real Element of ExtREAL
integral (X,S,M,f) is ext-real Element of ExtREAL
integral (X,S,M,g) is ext-real Element of ExtREAL
(integral (X,S,M,f)) + (integral (X,S,M,g)) is ext-real Element of ExtREAL
(dom f) /\ (dom f) is set
c is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
F is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
a is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom a is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
dom c is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
M * c is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
Sum a is ext-real Element of ExtREAL
len F is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
b is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
z is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
x is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom x is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
dom b is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
M * b is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
Sum x is ext-real Element of ExtREAL
len z is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
dom z is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
(len z) * (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
k is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like set
len k is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
dom k is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Seg ((len z) * (len F)) is V37() V44((len z) * (len F)) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
dom F is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
a1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
a1 -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(a1 -' 1) div (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((a1 -' 1) div (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(a1 -' 1) mod (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((a1 -' 1) mod (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((len z) * (len F)) -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(((len z) * (len F)) -' 1) div (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
FG is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
FG is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
FG * FG is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
0 + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(FG * FG) -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((FG * FG) -' 1) div FG is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(FG * FG) div FG is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((FG * FG) div FG) - 1 is V22() V23() ext-real set
((len z) * (len F)) div (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
Seg x1 is V37() V44(x1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
b . (((a1 -' 1) div (len F)) + 1) is set
rng b is set
c1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
(a1 -' 1) mod c1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg c1 is V37() V44(c1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
c . (((a1 -' 1) mod (len F)) + 1) is set
rng c is set
(b . (((a1 -' 1) div (len F)) + 1)) /\ (c . (((a1 -' 1) mod (len F)) + 1)) is set
k . a1 is set
FG is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of S
dom FG is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
b1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
y1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
FG . b1 is set
FG . y1 is set
y1 -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(y1 -' 1) mod (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((y1 -' 1) mod (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(y1 -' 1) div (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((y1 -' 1) div (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
b1 -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(b1 -' 1) mod (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((b1 -' 1) mod (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(b1 -' 1) div (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((b1 -' 1) div (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
b . (((b1 -' 1) div (len F)) + 1) is set
c . (((b1 -' 1) mod (len F)) + 1) is set
(b . (((b1 -' 1) div (len F)) + 1)) /\ (c . (((b1 -' 1) mod (len F)) + 1)) is set
a1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
FG is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
FG * a1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
(FG * a1) -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((FG * a1) -' 1) div a1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(FG * a1) div a1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((FG * a1) div a1) - 1 is V22() V23() ext-real set
(((len z) * (len F)) div (len F)) - 1 is V22() V23() ext-real set
lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
Seg lb9 is V37() V44(lb9) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
(y1 -' 1) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(((y1 -' 1) div (len F)) + 1) - 1 is V22() V23() ext-real set
k is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
((((y1 -' 1) div (len F)) + 1) - 1) * k is V22() V23() ext-real set
(((y1 -' 1) mod (len F)) + 1) - 1 is V22() V23() ext-real set
(((((y1 -' 1) div (len F)) + 1) - 1) * k) + ((((y1 -' 1) mod (len F)) + 1) - 1) is V22() V23() ext-real set
((((((y1 -' 1) div (len F)) + 1) - 1) * k) + ((((y1 -' 1) mod (len F)) + 1) - 1)) + 1 is V22() V23() ext-real set
y1 - 1 is V22() V23() ext-real set
(y1 - 1) + 1 is V22() V23() ext-real set
(((((y1 -' 1) div (len F)) + 1) - 1) * k) + (((y1 -' 1) mod (len F)) + 1) is V22() V23() ext-real set
(b1 -' 1) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(((b1 -' 1) div (len F)) + 1) - 1 is V22() V23() ext-real set
((((b1 -' 1) div (len F)) + 1) - 1) * k is V22() V23() ext-real set
(((b1 -' 1) mod (len F)) + 1) - 1 is V22() V23() ext-real set
(((((b1 -' 1) div (len F)) + 1) - 1) * k) + ((((b1 -' 1) mod (len F)) + 1) - 1) is V22() V23() ext-real set
((((((b1 -' 1) div (len F)) + 1) - 1) * k) + ((((b1 -' 1) mod (len F)) + 1) - 1)) + 1 is V22() V23() ext-real set
b1 - 1 is V22() V23() ext-real set
(b1 - 1) + 1 is V22() V23() ext-real set
(((((b1 -' 1) div (len F)) + 1) - 1) * k) + (((b1 -' 1) mod (len F)) + 1) is V22() V23() ext-real set
k is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
(y1 -' 1) mod k is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg k is V37() V44(k) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
(b1 -' 1) mod k is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
lb9 * k is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
(lb9 * k) -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(y1 -' 1) div k is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(lb9 * k) div k is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((lb9 * k) div k) - 1 is V22() V23() ext-real set
((y1 -' 1) div k) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
b . (((y1 -' 1) div (len F)) + 1) is set
(FG . b1) /\ (FG . y1) is set
c . (((y1 -' 1) mod (len F)) + 1) is set
(b . (((y1 -' 1) div (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1)) is set
((b . (((b1 -' 1) div (len F)) + 1)) /\ (c . (((b1 -' 1) mod (len F)) + 1))) /\ ((b . (((y1 -' 1) div (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1))) is set
(c . (((b1 -' 1) mod (len F)) + 1)) /\ ((b . (((y1 -' 1) div (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1))) is set
(b . (((b1 -' 1) div (len F)) + 1)) /\ ((c . (((b1 -' 1) mod (len F)) + 1)) /\ ((b . (((y1 -' 1) div (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1)))) is set
(c . (((b1 -' 1) mod (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1)) is set
(b . (((y1 -' 1) div (len F)) + 1)) /\ ((c . (((b1 -' 1) mod (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1))) is set
(b . (((b1 -' 1) div (len F)) + 1)) /\ ((b . (((y1 -' 1) div (len F)) + 1)) /\ ((c . (((b1 -' 1) mod (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1)))) is set
(b . (((b1 -' 1) div (len F)) + 1)) /\ (b . (((y1 -' 1) div (len F)) + 1)) is set
((b . (((b1 -' 1) div (len F)) + 1)) /\ (b . (((y1 -' 1) div (len F)) + 1))) /\ ((c . (((b1 -' 1) mod (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1))) is set
{} /\ ((c . (((b1 -' 1) mod (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1))) is set
c . (((y1 -' 1) mod (len F)) + 1) is set
(FG . b1) /\ (FG . y1) is set
b . (((y1 -' 1) div (len F)) + 1) is set
(b . (((y1 -' 1) div (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1)) is set
((b . (((b1 -' 1) div (len F)) + 1)) /\ (c . (((b1 -' 1) mod (len F)) + 1))) /\ ((b . (((y1 -' 1) div (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1))) is set
(c . (((b1 -' 1) mod (len F)) + 1)) /\ ((b . (((y1 -' 1) div (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1))) is set
(b . (((b1 -' 1) div (len F)) + 1)) /\ ((c . (((b1 -' 1) mod (len F)) + 1)) /\ ((b . (((y1 -' 1) div (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1)))) is set
(c . (((b1 -' 1) mod (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1)) is set
(b . (((y1 -' 1) div (len F)) + 1)) /\ ((c . (((b1 -' 1) mod (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1))) is set
(b . (((b1 -' 1) div (len F)) + 1)) /\ ((b . (((y1 -' 1) div (len F)) + 1)) /\ ((c . (((b1 -' 1) mod (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1)))) is set
(b . (((b1 -' 1) div (len F)) + 1)) /\ (b . (((y1 -' 1) div (len F)) + 1)) is set
((b . (((b1 -' 1) div (len F)) + 1)) /\ (b . (((y1 -' 1) div (len F)) + 1))) /\ ((c . (((b1 -' 1) mod (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1))) is set
((b . (((b1 -' 1) div (len F)) + 1)) /\ (b . (((y1 -' 1) div (len F)) + 1))) /\ {} is set
FG is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
len FG is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
a1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
len a1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
dom a1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
b1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
len b1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
dom b1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
union (rng b) is set
Seg (len FG) is V37() V44( len FG) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
dom FG is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
c1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
FG . c1 is set
a1 . c1 is ext-real Element of ExtREAL
c1 -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(c1 -' 1) div (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((c1 -' 1) div (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
y1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
y1 * x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
(y1 * x1) -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((y1 * x1) -' 1) div x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(y1 * x1) div x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((y1 * x1) div x1) - 1 is V22() V23() ext-real set
Seg (len z) is V37() V44( len z) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x is set
f . x is ext-real Element of ExtREAL
b . (((c1 -' 1) div (len F)) + 1) is set
(c1 -' 1) mod (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((c1 -' 1) mod (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
c . (((c1 -' 1) mod (len F)) + 1) is set
(b . (((c1 -' 1) div (len F)) + 1)) /\ (c . (((c1 -' 1) mod (len F)) + 1)) is set
z . (((c1 -' 1) div (len F)) + 1) is ext-real Element of ExtREAL
y1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
FG . y1 is set
b1 . y1 is ext-real Element of ExtREAL
y1 -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(y1 -' 1) mod (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((y1 -' 1) mod (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg (len F) is V37() V44( len F) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
c1 is set
g . c1 is ext-real Element of ExtREAL
(y1 -' 1) div (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((y1 -' 1) div (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
b . (((y1 -' 1) div (len F)) + 1) is set
c . (((y1 -' 1) mod (len F)) + 1) is set
(b . (((y1 -' 1) div (len F)) + 1)) /\ (c . (((y1 -' 1) mod (len F)) + 1)) is set
F . (((y1 -' 1) mod (len F)) + 1) is ext-real Element of ExtREAL
union (rng c) is set
rng FG is set
union (rng FG) is set
y1 is set
x1 is set
c1 is set
z1 is set
c . z1 is set
x is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg (len F) is V37() V44( len F) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
1 + lb9 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
k is set
b . k is set
p is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg (len z) is V37() V44( len z) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
q is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
1 + q is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
p - 1 is V22() V23() ext-real set
(p - 1) * (len F) is V22() V23() ext-real set
((p - 1) * (len F)) + x is V22() V23() ext-real set
0 + x is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
EMPTY is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
EMPTY -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
EMPTY - 1 is V22() V23() ext-real set
q * (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(q * (len F)) + lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(EMPTY -' 1) div (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((EMPTY -' 1) div (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(len z) - 1 is V22() V23() ext-real set
((len z) - 1) * (len F) is V22() V23() ext-real set
(((len z) - 1) * (len F)) + x is V22() V23() ext-real set
(((len z) - 1) * (len F)) + (len F) is V22() V23() ext-real set
FG . EMPTY is set
(EMPTY -' 1) mod (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((EMPTY -' 1) mod (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
b . p is set
c . x is set
(b . p) /\ (c . x) is set
c1 is set
z1 is set
x is set
FG . x is set
lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
lb9 -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(lb9 -' 1) mod (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((lb9 -' 1) mod (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(lb9 -' 1) div (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((lb9 -' 1) div (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
FG . lb9 is set
b . (((lb9 -' 1) div (len F)) + 1) is set
c . (((lb9 -' 1) mod (len F)) + 1) is set
(b . (((lb9 -' 1) div (len F)) + 1)) /\ (c . (((lb9 -' 1) mod (len F)) + 1)) is set
x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
y1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
y1 * x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
(y1 * x1) -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((y1 * x1) -' 1) div x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(y1 * x1) div x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((y1 * x1) div x1) - 1 is V22() V23() ext-real set
(((len z) * (len F)) div (len F)) - 1 is V22() V23() ext-real set
q is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
Seg (len z) is V37() V44( len z) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
b . q is set
c1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
FG . c1 is set
z1 is Element of X
x is Element of X
(f + g) . z1 is ext-real Element of ExtREAL
(f + g) . x is ext-real Element of ExtREAL
c1 -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(c1 -' 1) mod (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((c1 -' 1) mod (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(c1 -' 1) div (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((c1 -' 1) div (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
b . (((c1 -' 1) div (len F)) + 1) is set
c . (((c1 -' 1) mod (len F)) + 1) is set
(b . (((c1 -' 1) div (len F)) + 1)) /\ (c . (((c1 -' 1) mod (len F)) + 1)) is set
x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
y1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
y1 * x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
(y1 * x1) -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((y1 * x1) -' 1) div x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(y1 * x1) div x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((y1 * x1) div x1) - 1 is V22() V23() ext-real set
(((len z) * (len F)) div (len F)) - 1 is V22() V23() ext-real set
Seg (len z) is V37() V44( len z) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
f . z1 is ext-real Element of ExtREAL
z . (((c1 -' 1) div (len F)) + 1) is ext-real Element of ExtREAL
Seg (len F) is V37() V44( len F) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
f . x is ext-real Element of ExtREAL
g . z1 is ext-real Element of ExtREAL
(f . z1) + (g . z1) is ext-real Element of ExtREAL
F . (((c1 -' 1) mod (len F)) + 1) is ext-real Element of ExtREAL
(z . (((c1 -' 1) div (len F)) + 1)) + (F . (((c1 -' 1) mod (len F)) + 1)) is ext-real Element of ExtREAL
g . x is ext-real Element of ExtREAL
(f . x) + (g . x) is ext-real Element of ExtREAL
M * FG is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
y1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
len y1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
dom y1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
y1 . x1 is ext-real Element of ExtREAL
b1 . x1 is ext-real Element of ExtREAL
(M * FG) . x1 is ext-real Element of ExtREAL
(b1 . x1) * ((M * FG) . x1) is ext-real Element of ExtREAL
y1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom y1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
y1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom y1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
len x1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
dom x1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
c1 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x1 . c1 is ext-real Element of ExtREAL
a1 . c1 is ext-real Element of ExtREAL
(M * FG) . c1 is ext-real Element of ExtREAL
(a1 . c1) * ((M * FG) . c1) is ext-real Element of ExtREAL
x1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom x1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom x1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Seg (len a1) is V37() V44( len a1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Sum x1 is ext-real Element of ExtREAL
c1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
len c1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
dom c1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
z1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
len z1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
dom z1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
z1 . x is ext-real Element of ExtREAL
c1 . x is ext-real Element of ExtREAL
(M * FG) . x is ext-real Element of ExtREAL
(c1 . x) * ((M * FG) . x) is ext-real Element of ExtREAL
z1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom z1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
z1 is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom z1 is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
FG . x is set
c1 . x is ext-real Element of ExtREAL
lb9 is set
(f + g) . lb9 is ext-real Element of ExtREAL
f . lb9 is ext-real Element of ExtREAL
g . lb9 is ext-real Element of ExtREAL
(f . lb9) + (g . lb9) is ext-real Element of ExtREAL
a1 . x is ext-real Element of ExtREAL
(a1 . x) + (g . lb9) is ext-real Element of ExtREAL
b1 . x is ext-real Element of ExtREAL
(a1 . x) + (b1 . x) is ext-real Element of ExtREAL
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
y1 . x is ext-real Element of ExtREAL
x -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(x -' 1) mod (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((x -' 1) mod (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
b1 . x is ext-real Element of ExtREAL
(M * FG) . x is ext-real Element of ExtREAL
(b1 . x) * ((M * FG) . x) is ext-real Element of ExtREAL
Seg (len F) is V37() V44( len F) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
c . (((x -' 1) mod (len F)) + 1) is set
k is set
FG . x is set
q is Element of S
p is Element of S
M . {} is ext-real Element of ExtREAL
M . p is ext-real Element of ExtREAL
g . k is ext-real Element of ExtREAL
F . (((x -' 1) mod (len F)) + 1) is ext-real Element of ExtREAL
c . (((x -' 1) mod (len F)) + 1) is set
FG . x is set
(x -' 1) div (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((x -' 1) div (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
b . (((x -' 1) div (len F)) + 1) is set
(b . (((x -' 1) div (len F)) + 1)) /\ (c . (((x -' 1) mod (len F)) + 1)) is set
M . (FG . x) is ext-real Element of ExtREAL
c . (((x -' 1) mod (len F)) + 1) is set
rng y1 is V86() set
x is set
y1 . x is ext-real Element of ExtREAL
x1 " {+infty} is set
y1 " {-infty} is set
(x1 " {+infty}) /\ (y1 " {-infty}) is set
(x1 " {+infty}) /\ {} is set
k is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x1 . k is ext-real Element of ExtREAL
k -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(k -' 1) div (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((k -' 1) div (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
a1 . k is ext-real Element of ExtREAL
(M * FG) . k is ext-real Element of ExtREAL
(a1 . k) * ((M * FG) . k) is ext-real Element of ExtREAL
lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x * lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
(x * lb9) -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((x * lb9) -' 1) div lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(x * lb9) div lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((x * lb9) div lb9) - 1 is V22() V23() ext-real set
(((len z) * (len F)) div (len F)) - 1 is V22() V23() ext-real set
Seg (len z) is V37() V44( len z) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
b . (((k -' 1) div (len F)) + 1) is set
q is set
FG . k is set
EMPTY is Element of S
v is Element of S
M . {} is ext-real Element of ExtREAL
M . v is ext-real Element of ExtREAL
f . q is ext-real Element of ExtREAL
z . (((k -' 1) div (len F)) + 1) is ext-real Element of ExtREAL
b . (((k -' 1) div (len F)) + 1) is set
FG . k is set
(k -' 1) mod (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((k -' 1) mod (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
c . (((k -' 1) mod (len F)) + 1) is set
(b . (((k -' 1) div (len F)) + 1)) /\ (c . (((k -' 1) mod (len F)) + 1)) is set
M . (FG . k) is ext-real Element of ExtREAL
b . (((k -' 1) div (len F)) + 1) is set
rng x1 is V86() set
x is set
x1 . x is ext-real Element of ExtREAL
x1 " {-infty} is set
y1 " {+infty} is set
(x1 " {-infty}) /\ (y1 " {+infty}) is set
{} /\ (y1 " {+infty}) is set
x1 + y1 is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
dom (x1 + y1) is set
(dom x1) /\ (dom y1) is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
{} \/ {} is set
((dom x1) /\ (dom y1)) \ ({} \/ {}) is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
k is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
z1 . k is ext-real Element of ExtREAL
(x1 + y1) . k is ext-real Element of ExtREAL
k -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(k -' 1) div (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((k -' 1) div (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(k -' 1) mod (len F) is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((k -' 1) mod (len F)) + 1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x * lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
(x * lb9) -' 1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((x * lb9) -' 1) div lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
(x * lb9) div lb9 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
((x * lb9) div lb9) - 1 is V22() V23() ext-real set
(((len z) * (len F)) div (len F)) - 1 is V22() V23() ext-real set
Seg (len z) is V37() V44( len z) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Seg (len F) is V37() V44( len F) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
a1 . k is ext-real Element of ExtREAL
b1 . k is ext-real Element of ExtREAL
(a1 . k) + (b1 . k) is ext-real Element of ExtREAL
(M * FG) . k is ext-real Element of ExtREAL
((a1 . k) + (b1 . k)) * ((M * FG) . k) is ext-real Element of ExtREAL
(a1 . k) * ((M * FG) . k) is ext-real Element of ExtREAL
(b1 . k) * ((M * FG) . k) is ext-real Element of ExtREAL
((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) is ext-real Element of ExtREAL
FG . k is set
b . (((k -' 1) div (len F)) + 1) is set
c . (((k -' 1) mod (len F)) + 1) is set
(b . (((k -' 1) div (len F)) + 1)) /\ (c . (((k -' 1) mod (len F)) + 1)) is set
v is set
F . (((k -' 1) mod (len F)) + 1) is ext-real Element of ExtREAL
g . v is ext-real Element of ExtREAL
z . (((k -' 1) div (len F)) + 1) is ext-real Element of ExtREAL
f . v is ext-real Element of ExtREAL
FG . k is set
M . (FG . k) is ext-real Element of ExtREAL
FG . k is set
c1 . k is ext-real Element of ExtREAL
(c1 . k) * ((M * FG) . k) is ext-real Element of ExtREAL
x1 . k is ext-real Element of ExtREAL
(x1 . k) + ((b1 . k) * ((M * FG) . k)) is ext-real Element of ExtREAL
y1 . k is ext-real Element of ExtREAL
(x1 . k) + (y1 . k) is ext-real Element of ExtREAL
(dom g) /\ (dom g) is set
x is Element of X
(f + g) . x is ext-real Element of ExtREAL
|.((f + g) . x).| is ext-real Element of ExtREAL
f . x is ext-real Element of ExtREAL
g . x is ext-real Element of ExtREAL
(f . x) + (g . x) is ext-real Element of ExtREAL
|.((f . x) + (g . x)).| is ext-real Element of ExtREAL
|.(f . x).| is ext-real Element of ExtREAL
|.(g . x).| is ext-real Element of ExtREAL
|.(f . x).| + |.(g . x).| is ext-real Element of ExtREAL
x is set
(f + g) . x is ext-real Element of ExtREAL
f . x is ext-real Element of ExtREAL
g . x is ext-real Element of ExtREAL
(f . x) + (g . x) is ext-real Element of ExtREAL
Sum z1 is ext-real Element of ExtREAL
len z1 is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
Seg (len z1) is V37() V44( len z1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Seg (len b1) is V37() V44( len b1) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Sum y1 is ext-real Element of ExtREAL
X is non empty set
K19(X) is set
K19(K19(X)) is set
K20(X,ExtREAL) is V62() set
K19(K20(X,ExtREAL)) is set
S is non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive Element of K19(K19(X))
K20(S,ExtREAL) is V62() set
K19(K20(S,ExtREAL)) is set
M is Relation-like S -defined ExtREAL -valued Function-like V30(S, ExtREAL ) V62() V70() nonnegative sigma-additive Element of K19(K20(S,ExtREAL))
f is Relation-like X -defined ExtREAL -valued Function-like V62() Element of K19(K20(X,ExtREAL))
dom f is set
g is Relation-like X -defined ExtREAL -valued Function-like V62() Element of K19(K20(X,ExtREAL))
dom g is set
integral (X,S,M,g) is ext-real Element of ExtREAL
integral (X,S,M,f) is ext-real Element of ExtREAL
c is ext-real Element of ExtREAL
c * (integral (X,S,M,f)) is ext-real Element of ExtREAL
F is set
g . F is ext-real Element of ExtREAL
f . F is ext-real Element of ExtREAL
c * (f . F) is ext-real Element of ExtREAL
F is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
rng F is set
union (rng F) is set
dom F is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
a is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
F . a is set
x is Element of X
b is Element of X
g . x is ext-real Element of ExtREAL
g . b is ext-real Element of ExtREAL
f . b is ext-real Element of ExtREAL
c * (f . b) is ext-real Element of ExtREAL
f . x is ext-real Element of ExtREAL
c * (f . x) is ext-real Element of ExtREAL
a is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x is Element of X
F . a is set
b is Element of X
g . x is ext-real Element of ExtREAL
g . b is ext-real Element of ExtREAL
F is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
a is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
x is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom x is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
dom F is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
M * F is Relation-like NAT -defined ExtREAL -valued Function-like V62() Element of K19(K20(NAT,ExtREAL))
Sum x is ext-real Element of ExtREAL
dom a is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
len a is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
b is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like set
len b is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
dom b is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
rng b is set
z is set
x is set
b . x is set
x is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
a . x is ext-real Element of ExtREAL
c * (a . x) is ext-real Element of ExtREAL
Seg (len b) is V37() V44( len b) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
z is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom z is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
z . x is ext-real Element of ExtREAL
a . x is ext-real Element of ExtREAL
c * (a . x) is ext-real Element of ExtREAL
b is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom b is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
b is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom b is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
len x is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
z is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like set
len z is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
dom z is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
rng z is set
x is set
x is set
z . x is set
k is V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() Element of NAT
x . k is ext-real Element of ExtREAL
c * (x . k) is ext-real Element of ExtREAL
Seg (len z) is V37() V44( len z) V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom x is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x . x is ext-real Element of ExtREAL
x . x is ext-real Element of ExtREAL
c * (x . x) is ext-real Element of ExtREAL
z is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom z is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
z is Relation-like NAT -defined ExtREAL -valued Function-like V37() FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom z is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
z . x is ext-real Element of ExtREAL
b . x is ext-real Element of ExtREAL
(M * F) . x is ext-real Element of ExtREAL
(b . x) * ((M * F) . x) is ext-real Element of ExtREAL
x . x is ext-real Element of ExtREAL
c * (x . x) is ext-real Element of ExtREAL
a . x is ext-real Element of ExtREAL
(a . x) * ((M * F) . x) is ext-real Element of ExtREAL
c * ((a . x) * ((M * F) . x)) is ext-real Element of ExtREAL
c * (a . x) is ext-real Element of ExtREAL
(c * (a . x)) * ((M * F) . x) is ext-real Element of ExtREAL
rng F is set
union (rng F) is set
x is V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() set
x is set
F . x is set
g . x is ext-real Element of ExtREAL
f . x is ext-real Element of ExtREAL
c * (f . x) is ext-real Element of ExtREAL
a . x is ext-real Element of ExtREAL
c * (a . x) is ext-real Element of ExtREAL
b . x is ext-real Element of ExtREAL
x is Element of X
g . x is ext-real Element of ExtREAL
|.(g . x).| is ext-real Element of ExtREAL
f . x is ext-real Element of ExtREAL
c * (f . x) is ext-real Element of ExtREAL
- +infty is non empty ext-real non positive negative Element of ExtREAL
x is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like V83() FinSequence of S
rng x is set
union (rng x) is set
dom x is V85() V86() V87() V88() V89() V90() Element of K19(NAT)
Sum z is ext-real Element of ExtREAL