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