:: MESFUNC3 semantic presentation

REAL is non empty non trivial non finite V81() V82() V83() V87() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V61() V62() V81() V82() V83() V84() V85() V86() V87() Element of bool REAL
bool REAL is non empty non trivial non finite set
ExtREAL is non empty V82() set
[:NAT,ExtREAL:] is Relation-like non empty non trivial non finite V72() set
bool [:NAT,ExtREAL:] is non empty non trivial non finite set
bool ExtREAL is non empty set
RAT is non empty non trivial non finite V81() V82() V83() V84() V87() set
{} is set
the Relation-like non-empty empty-yielding RAT -valued functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real non positive non negative finite finite-yielding V47() cardinal {} -element FinSequence-like FinSequence-membered V61() V71() V72() V73() V74() V81() V82() V83() V84() V85() V86() V87() set is Relation-like non-empty empty-yielding RAT -valued functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real non positive non negative finite finite-yielding V47() cardinal {} -element FinSequence-like FinSequence-membered V61() V71() V72() V73() V74() V81() V82() V83() V84() V85() V86() V87() set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V61() V62() V81() V82() V83() V84() V85() V86() V87() set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
[:NAT,REAL:] is Relation-like non empty non trivial non finite V71() V72() V73() set
bool [:NAT,REAL:] is non empty non trivial non finite set
bool (bool REAL) is non empty non trivial non finite set
K101(NAT) is V27() set
COMPLEX is non empty non trivial non finite V81() V87() set
INT is non empty non trivial non finite V81() V82() V83() V84() V85() V87() set
[:REAL,REAL:] is Relation-like non empty non trivial non finite V71() V72() V73() set
bool [:REAL,REAL:] is non empty non trivial non finite set
bool RAT is non empty non trivial non finite set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial non finite V71() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial non finite V71() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial non finite V71() V72() V73() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial non finite V71() V72() V73() set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial non finite V71() V72() V73() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V71() V72() V73() set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V71() V72() V73() set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V71() V72() V73() V74() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V71() V72() V73() V74() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
K519() is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
{{},1} is finite V61() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
0. is ext-real Element of ExtREAL
<*> ExtREAL is Relation-like non-empty empty-yielding NAT -defined ExtREAL -valued Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real non positive non negative finite finite-yielding V47() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V58() V61() V71() V72() V73() V74() V81() V82() V83() V84() V85() V86() V87() FinSequence of ExtREAL
Sum (<*> ExtREAL) is ext-real Element of ExtREAL
-infty is non empty non real ext-real non positive negative Element of ExtREAL
Seg 1 is non empty trivial finite 1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
{1} is non empty trivial finite V47() 1 -element V61() V81() V82() V83() V84() V85() V86() set
Seg 2 is non empty finite 2 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
{1,2} is finite V47() V61() V81() V82() V83() V84() V85() V86() set
diffreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty total V18([:REAL,REAL:], REAL ) V71() V72() V73() Element of bool [:[:REAL,REAL:],REAL:]
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real non positive non negative finite finite-yielding V47() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V58() V61() V71() V72() V73() V74() V81() V82() V83() V84() V85() V86() V87() FinSequence of REAL
Sum (<*> REAL) is V36() real ext-real Element of REAL
+infty is non empty non real ext-real positive non negative Element of ExtREAL
+infty is non empty non real ext-real positive non negative set
-infty is non empty non real ext-real non positive negative set
X is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
Seg X is finite X -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
Seg (X + 1) is non empty finite X + 1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
S is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
Seg (S + 1) is non empty finite S + 1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
M is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
Seg M is finite M -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
[:(Seg (S + 1)),(Seg M):] is Relation-like RAT -valued INT -valued finite V61() V71() V72() V73() V74() set
[:[:(Seg (S + 1)),(Seg M):],REAL:] is Relation-like V71() V72() V73() set
bool [:[:(Seg (S + 1)),(Seg M):],REAL:] is non empty set
s1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom s1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
f is Relation-like [:(Seg (S + 1)),(Seg M):] -defined REAL -valued Function-like total V18([:(Seg (S + 1)),(Seg M):], REAL ) finite V61() V71() V72() V73() Element of bool [:[:(Seg (S + 1)),(Seg M):],REAL:]
s2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom s2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Seg S is finite S -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
[:(Seg S),(Seg M):] is Relation-like RAT -valued INT -valued finite V61() V71() V72() V73() V74() set
f | [:(Seg S),(Seg M):] is Relation-like [:(Seg (S + 1)),(Seg M):] -defined [:(Seg S),(Seg M):] -defined [:(Seg (S + 1)),(Seg M):] -defined REAL -valued Function-like finite V61() V71() V72() V73() Element of bool [:[:(Seg (S + 1)),(Seg M):],REAL:]
[:[:(Seg S),(Seg M):],REAL:] is Relation-like V71() V72() V73() set
bool [:[:(Seg S),(Seg M):],REAL:] is non empty set
s1 | (Seg S) is Relation-like NAT -defined Seg S -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like V61() V71() V72() V73() Element of bool [:NAT,REAL:]
len s1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
x2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom x2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
F1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
s1 . F1 is V36() real ext-real Element of REAL
a1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom a1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum a1 is V36() real ext-real Element of REAL
x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom x1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x2 . F1 is V36() real ext-real Element of REAL
Sum x1 is V36() real ext-real Element of REAL
a2 is Relation-like [:(Seg S),(Seg M):] -defined REAL -valued Function-like total V18([:(Seg S),(Seg M):], REAL ) finite V61() V71() V72() V73() Element of bool [:[:(Seg S),(Seg M):],REAL:]
dom f is Relation-like Seg (S + 1) -defined Seg M -valued finite V61() V71() V72() V73() V74() Element of bool [:(Seg (S + 1)),(Seg M):]
bool [:(Seg (S + 1)),(Seg M):] is non empty finite V47() V61() set
dom a2 is Relation-like Seg S -defined Seg M -valued finite V61() V71() V72() V73() V74() Element of bool [:(Seg S),(Seg M):]
bool [:(Seg S),(Seg M):] is non empty finite V47() V61() set
[:(Seg (S + 1)),(Seg M):] /\ [:(Seg S),(Seg M):] is Relation-like RAT -valued INT -valued finite V61() V71() V72() V73() V74() set
m is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
x1 . m is V36() real ext-real Element of REAL
[F1,m] is set
{F1,m} is finite V47() V61() V81() V82() V83() V84() V85() V86() set
{F1} is non empty trivial finite V47() 1 -element V61() V81() V82() V83() V84() V85() V86() set
{{F1,m},{F1}} is finite V47() V61() set
a2 . [F1,m] is V36() real ext-real Element of REAL
f . [F1,m] is V36() real ext-real Element of REAL
F1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
a1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V61() set
len a1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
dom a1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
a1 . x1 is set
[(S + 1),x1] is set
{(S + 1),x1} is finite V47() V61() V81() V82() V83() V84() V85() V86() set
{(S + 1)} is non empty trivial finite V47() 1 -element V61() V81() V82() V83() V84() V85() V86() set
{{(S + 1),x1},{(S + 1)}} is finite V47() V61() set
f . [(S + 1),x1] is V36() real ext-real Element of REAL
Seg F1 is finite F1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
F1 -tuples_on REAL is FinSequenceSet of REAL
dom x1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum x1 is V36() real ext-real Element of REAL
s1 . (S + 1) is V36() real ext-real Element of REAL
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom m is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum m is V36() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
m . n is V36() real ext-real Element of REAL
[(S + 1),n] is set
{(S + 1),n} is finite V47() V61() V81() V82() V83() V84() V85() V86() set
{{(S + 1),n},{(S + 1)}} is finite V47() V61() set
f . [(S + 1),n] is V36() real ext-real Element of REAL
x1 . n is V36() real ext-real Element of REAL
s2 - x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
<:s2,x1:> is Relation-like Function-like set
rng <:s2,x1:> is set
rng s2 is finite V61() V81() V82() V83() Element of bool REAL
rng x1 is finite V61() V81() V82() V83() Element of bool REAL
[:(rng s2),(rng x1):] is Relation-like finite V61() V71() V72() V73() set
dom diffreal is Relation-like REAL -defined REAL -valued non empty V71() V72() V73() Element of bool [:REAL,REAL:]
diffreal .: (s2,x1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom (diffreal .: (s2,x1)) is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
<:s2,x1:> * diffreal is Relation-like REAL -valued V71() V72() V73() set
dom (<:s2,x1:> * diffreal) is set
dom <:s2,x1:> is set
(dom s2) /\ (dom x1) is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom m is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
(Seg F1) /\ (Seg F1) is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
len m is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
s2 . n is V36() real ext-real Element of REAL
a is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom a is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum a is V36() real ext-real Element of REAL
a . (S + 1) is V36() real ext-real Element of REAL
[(S + 1),n] is set
{(S + 1),n} is finite V47() V61() V81() V82() V83() V84() V85() V86() set
{{(S + 1),n},{(S + 1)}} is finite V47() V61() set
f . [(S + 1),n] is V36() real ext-real Element of REAL
x1 . n is V36() real ext-real Element of REAL
a | (Seg S) is Relation-like NAT -defined Seg S -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like V61() V71() V72() V73() Element of bool [:NAT,REAL:]
p is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
len a is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
q is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom q is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
<*(a . (S + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V61() V71() V72() V73() V75() V76() V77() V78() FinSequence of REAL
q ^ <*(a . (S + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
(s2 . n) - (x1 . n) is V36() real ext-real Element of REAL
Sum q is V36() real ext-real Element of REAL
(Sum q) + (x1 . n) is V36() real ext-real Element of REAL
((Sum q) + (x1 . n)) - (x1 . n) is V36() real ext-real Element of REAL
m . n is V36() real ext-real Element of REAL
dom f is Relation-like Seg (S + 1) -defined Seg M -valued finite V61() V71() V72() V73() V74() Element of bool [:(Seg (S + 1)),(Seg M):]
bool [:(Seg (S + 1)),(Seg M):] is non empty finite V47() V61() set
[:(Seg (S + 1)),(Seg F1):] is Relation-like RAT -valued INT -valued finite V61() V71() V72() V73() V74() set
dom a2 is Relation-like Seg S -defined Seg M -valued finite V61() V71() V72() V73() V74() Element of bool [:(Seg S),(Seg M):]
bool [:(Seg S),(Seg M):] is non empty finite V47() V61() set
[:(Seg S),(Seg F1):] is Relation-like RAT -valued INT -valued finite V61() V71() V72() V73() V74() set
[:(Seg (S + 1)),(Seg F1):] /\ [:(Seg S),(Seg F1):] is Relation-like RAT -valued INT -valued finite V61() V71() V72() V73() V74() set
k is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
q . k is V36() real ext-real Element of REAL
[k,n] is set
{k,n} is finite V47() V61() V81() V82() V83() V84() V85() V86() set
{k} is non empty trivial finite V47() 1 -element V61() V81() V82() V83() V84() V85() V86() set
{{k,n},{k}} is finite V47() V61() set
a2 . [k,n] is V36() real ext-real Element of REAL
a . k is V36() real ext-real Element of REAL
f . [k,n] is V36() real ext-real Element of REAL
len s2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
m + x1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
<*(Sum x1)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V61() V71() V72() V73() V75() V76() V77() V78() FinSequence of REAL
x2 ^ <*(Sum x1)*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
Sum s1 is V36() real ext-real Element of REAL
Sum x2 is V36() real ext-real Element of REAL
(Sum x2) + (Sum x1) is V36() real ext-real Element of REAL
Sum m is V36() real ext-real Element of REAL
(Sum m) + (Sum x1) is V36() real ext-real Element of REAL
Sum s2 is V36() real ext-real Element of REAL
M is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
Seg M is finite M -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
[:(Seg (X + 1)),(Seg M):] is Relation-like RAT -valued INT -valued finite V61() V71() V72() V73() V74() set
[:[:(Seg (X + 1)),(Seg M):],REAL:] is Relation-like V71() V72() V73() set
bool [:[:(Seg (X + 1)),(Seg M):],REAL:] is non empty set
s1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom s1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
f is Relation-like [:(Seg (X + 1)),(Seg M):] -defined REAL -valued Function-like total V18([:(Seg (X + 1)),(Seg M):], REAL ) finite V61() V71() V72() V73() Element of bool [:[:(Seg (X + 1)),(Seg M):],REAL:]
s2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom s2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum s1 is V36() real ext-real Element of REAL
Sum s2 is V36() real ext-real Element of REAL
Seg 0 is Relation-like non-empty empty-yielding RAT -valued functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real non positive non negative finite finite-yielding V47() cardinal 0 -element FinSequence-like FinSequence-membered V61() V71() V72() V73() V74() V81() V82() V83() V84() V85() V86() V87() Element of bool NAT
X is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
Seg X is finite X -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
[:(Seg 0),(Seg X):] is Relation-like RAT -valued INT -valued finite V61() V71() V72() V73() V74() set
[:[:(Seg 0),(Seg X):],REAL:] is Relation-like V71() V72() V73() set
bool [:[:(Seg 0),(Seg X):],REAL:] is non empty set
M is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom M is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
S is Relation-like [:(Seg 0),(Seg X):] -defined REAL -valued Function-like total V18([:(Seg 0),(Seg X):], REAL ) finite V61() V71() V72() V73() Element of bool [:[:(Seg 0),(Seg X):],REAL:]
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom f is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
s2 is set
s1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT : ( 1 <= b₁ & b₁ <= s1 ) } is set
a2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
F2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
f . F2 is V36() real ext-real Element of REAL
a2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom a2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum a2 is V36() real ext-real Element of REAL
f . s2 is V36() real ext-real Element of REAL
(dom f) --> 0 is Relation-like dom f -defined NAT -valued RAT -valued INT -valued Function-like total V18( dom f, NAT ) finite V58() V61() V71() V72() V73() V74() Element of bool [:(dom f),NAT:]
[:(dom f),NAT:] is Relation-like RAT -valued INT -valued V71() V72() V73() V74() set
bool [:(dom f),NAT:] is non empty set
s1 |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() V74() Element of s1 -tuples_on NAT
s1 -tuples_on NAT is FinSequenceSet of NAT
Sum M is V36() real ext-real Element of REAL
Sum f is V36() real ext-real Element of REAL
X is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
Seg X is finite X -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
[:(Seg 0),(Seg X):] is Relation-like RAT -valued INT -valued finite V61() V71() V72() V73() V74() set
[:[:(Seg 0),(Seg X):],REAL:] is Relation-like V71() V72() V73() set
bool [:[:(Seg 0),(Seg X):],REAL:] is non empty set
M is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom M is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
S is Relation-like [:(Seg 0),(Seg X):] -defined REAL -valued Function-like total V18([:(Seg 0),(Seg X):], REAL ) finite V61() V71() V72() V73() Element of bool [:[:(Seg 0),(Seg X):],REAL:]
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom f is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum M is V36() real ext-real Element of REAL
Sum f is V36() real ext-real Element of REAL
X is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
Sum X is ext-real Element of ExtREAL
S is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
Sum S is V36() real ext-real Element of REAL
len X is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
Seg (len X) is finite len X -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
X | (Seg (len X)) is Relation-like NAT -defined Seg (len X) -defined NAT -defined ExtREAL -valued Function-like finite FinSubsequence-like V61() V72() Element of bool [:NAT,ExtREAL:]
X | (len X) is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
M is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
Seg M is finite M -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
X | (Seg M) is Relation-like NAT -defined Seg M -defined NAT -defined ExtREAL -valued Function-like finite FinSubsequence-like V61() V72() Element of bool [:NAT,ExtREAL:]
S | (Seg M) is Relation-like NAT -defined Seg M -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like V61() V71() V72() V73() Element of bool [:NAT,REAL:]
M + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
Seg (M + 1) is non empty finite M + 1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
X | (Seg (M + 1)) is Relation-like NAT -defined Seg (M + 1) -defined NAT -defined ExtREAL -valued Function-like finite FinSubsequence-like V61() V72() Element of bool [:NAT,ExtREAL:]
S | (Seg (M + 1)) is Relation-like NAT -defined Seg (M + 1) -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like V61() V71() V72() V73() Element of bool [:NAT,REAL:]
f is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
Sum f is ext-real Element of ExtREAL
s1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
Sum s1 is V36() real ext-real Element of REAL
s1 . (M + 1) is V36() real ext-real Element of REAL
<*(s1 . (M + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V61() V71() V72() V73() V75() V76() V77() V78() FinSequence of REAL
f | (Seg M) is Relation-like NAT -defined Seg M -defined NAT -defined ExtREAL -valued Function-like finite FinSubsequence-like V61() V72() Element of bool [:NAT,ExtREAL:]
s2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
rng s2 is finite V61() V81() V82() V83() Element of bool REAL
F2 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
rng F2 is finite V61() V82() Element of bool ExtREAL
f . (M + 1) is ext-real Element of ExtREAL
<*(f . (M + 1))*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V61() V72() V75() V76() V77() V78() FinSequence of ExtREAL
rng <*(f . (M + 1))*> is non empty trivial finite 1 -element V61() V82() Element of bool ExtREAL
s1 | (Seg M) is Relation-like NAT -defined Seg M -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like V61() V71() V72() V73() Element of bool [:NAT,REAL:]
len s1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
a2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
a2 ^ <*(s1 . (M + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
Sum a2 is V36() real ext-real Element of REAL
(Sum a2) + (s1 . (M + 1)) is V36() real ext-real Element of REAL
len f is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
F2 ^ <*(f . (M + 1))*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
Sum F2 is ext-real Element of ExtREAL
Sum <*(f . (M + 1))*> is ext-real Element of ExtREAL
(Sum F2) + (Sum <*(f . (M + 1))*>) is ext-real Element of ExtREAL
(Sum F2) + (f . (M + 1)) is ext-real Element of ExtREAL
f is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
s1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
Sum f is ext-real Element of ExtREAL
Sum s1 is V36() real ext-real Element of REAL
Seg 0 is Relation-like non-empty empty-yielding RAT -valued functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real non positive non negative finite finite-yielding V47() cardinal 0 -element FinSequence-like FinSequence-membered V61() V71() V72() V73() V74() V81() V82() V83() V84() V85() V86() V87() Element of bool NAT
X | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined ExtREAL -valued RAT -valued Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real non positive non negative finite finite-yielding V47() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V58() V61() V71() V72() V73() V74() V81() V82() V83() V84() V85() V86() V87() Element of bool [:NAT,ExtREAL:]
S | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined REAL -valued RAT -valued Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real non positive non negative finite finite-yielding V47() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V58() V61() V71() V72() V73() V74() V81() V82() V83() V84() V85() V86() V87() Element of bool [:NAT,REAL:]
M is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
Sum M is ext-real Element of ExtREAL
Sum f is V36() real ext-real Element of REAL
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is Relation-like non empty V72() set
bool [:X,ExtREAL:] is non empty set
S is non empty V24() V25() V26() compl-closed sigma-multiplicative sigma-additive Element of bool (bool X)
M is Relation-like X -defined ExtREAL -valued Function-like V72() Element of bool [:X,ExtREAL:]
dom M is Element of bool X
f is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng f is finite V61() Element of bool S
bool S is non empty set
union (rng f) is set
dom f is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
len f is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
Seg (len f) is finite len f -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
s1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
f . s1 is set
s2 is ext-real Element of ExtREAL
F2 is set
M . F2 is ext-real Element of ExtREAL
s2 is set
M . s2 is ext-real Element of ExtREAL
F2 is ext-real Element of ExtREAL
a2 is set
M . a2 is ext-real Element of ExtREAL
bool X is non empty Element of bool (bool X)
F1 is Element of X
M . F1 is ext-real Element of ExtREAL
x2 is Element of X
M . x2 is ext-real Element of ExtREAL
F2 is ext-real Element of ExtREAL
x2 is ext-real Element of ExtREAL
s1 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
dom s1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
s2 is set
F2 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
len F2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
dom F2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
a2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F2 . a2 is ext-real Element of ExtREAL
s1 . a2 is ext-real Element of ExtREAL
f . a2 is set
chi ((f . a2),X) is Relation-like X -defined ExtREAL -valued Function-like V72() Element of bool [:X,ExtREAL:]
(chi ((f . a2),X)) . s2 is ext-real Element of ExtREAL
(s1 . a2) * ((chi ((f . a2),X)) . s2) is ext-real Element of ExtREAL
s2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
f . s2 is set
s1 . s2 is ext-real Element of ExtREAL
F2 is set
M . F2 is ext-real Element of ExtREAL
s2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F2 is set
f . s2 is set
M . F2 is ext-real Element of ExtREAL
s1 . s2 is ext-real Element of ExtREAL
a2 is set
X is set
S is Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like V61() FinSequence of X
dom S is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
M is set
f is set
S . M is set
S . f is set
M is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
f is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
S . M is set
S . f is set
s1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
s2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
S . s1 is set
S . s2 is set
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
S is set
M is non empty V24() V25() V26() compl-closed sigma-multiplicative sigma-additive Element of bool (bool X)
f is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of M
dom f is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
s1 is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like V61() FinSequence of M
dom s1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
s2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
f . s2 is set
f . F2 is set
S /\ (f . s2) is set
S /\ (f . F2) is set
(S /\ (f . s2)) /\ (S /\ (f . F2)) is set
(f . s2) /\ (S /\ (f . F2)) is set
S /\ ((f . s2) /\ (S /\ (f . F2))) is set
(f . s2) /\ (f . F2) is set
((f . s2) /\ (f . F2)) /\ S is set
S /\ (((f . s2) /\ (f . F2)) /\ S) is set
{} /\ S is set
S /\ ({} /\ S) is set
s1 . s2 is set
s1 . F2 is set
X is non empty set
S is set
f is Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like V61() FinSequence of X
dom f is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
M is Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like V61() FinSequence of X
dom M is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
rng f is finite V61() Element of bool X
bool X is non empty set
union (rng f) is set
rng M is finite V61() Element of bool X
union (rng M) is set
S /\ (union (rng M)) is set
s1 is set
s2 is set
F2 is set
f . F2 is set
a2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
M . a2 is set
S /\ (M . a2) is set
s1 is set
s2 is set
F2 is set
M . F2 is set
S /\ s2 is set
a2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
f . a2 is set
X is set
S is Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like V61() FinSequence of X
dom S is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
rng S is finite V61() Element of bool X
bool X is non empty set
union (rng S) is set
M is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
S . M is set
(S . M) /\ (union (rng S)) is set
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
S is non empty V24() V25() V26() compl-closed sigma-multiplicative sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty V72() set
bool [:S,ExtREAL:] is non empty set
M is Relation-like S -defined ExtREAL -valued Function-like non empty total V18(S, ExtREAL ) V72() V80() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
dom f is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
M * f is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
dom (M * f) is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
dom M is non empty Element of bool S
bool S is non empty set
rng f is finite V61() Element of bool S
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
S is non empty V24() V25() V26() compl-closed sigma-multiplicative sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty V72() set
bool [:S,ExtREAL:] is non empty set
M is Relation-like S -defined ExtREAL -valued Function-like non empty total V18(S, ExtREAL ) V72() V80() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng f is finite V61() Element of bool S
bool S is non empty set
union (rng f) is set
M . (union (rng f)) is ext-real Element of ExtREAL
M * f is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
Sum (M * f) is ext-real Element of ExtREAL
s1 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
Sum s1 is ext-real Element of ExtREAL
len s1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
s2 is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) V72() Element of bool [:NAT,ExtREAL:]
s2 . (len s1) is ext-real Element of ExtREAL
s2 . 0 is ext-real Element of ExtREAL
[:NAT,S:] is Relation-like non empty non trivial non finite set
bool [:NAT,S:] is non empty non trivial non finite set
dom f is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
F2 is Relation-like NAT -defined S -valued Function-like non empty total V18( NAT ,S) disjoint_valued Element of bool [:NAT,S:]
rng F2 is non empty Element of bool (bool X)
union (rng F2) is Element of bool X
M * F2 is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) V72() Element of bool [:NAT,ExtREAL:]
Ser (M * F2) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) V72() Element of bool [:NAT,ExtREAL:]
rng (M * F2) is non empty V61() V82() Element of bool ExtREAL
dom F2 is non empty V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
a2 is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) V72() Num of rng (M * F2)
Ser ((rng (M * F2)),a2) is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) V72() Element of bool [:NAT,ExtREAL:]
x2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
x2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
(Ser (M * F2)) . (x2 + 1) is ext-real Element of ExtREAL
(Ser (M * F2)) . x2 is ext-real Element of ExtREAL
s1 . (x2 + 1) is ext-real Element of ExtREAL
((Ser (M * F2)) . x2) + (s1 . (x2 + 1)) is ext-real Element of ExtREAL
dom s1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
F1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
F1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
(Ser (M * F2)) . (F1 + 1) is ext-real Element of ExtREAL
(Ser (M * F2)) . F1 is ext-real Element of ExtREAL
a2 . (F1 + 1) is ext-real Element of ExtREAL
((Ser (M * F2)) . F1) + (a2 . (F1 + 1)) is ext-real Element of ExtREAL
F2 . (F1 + 1) is Element of S
M . (F2 . (F1 + 1)) is ext-real Element of ExtREAL
((Ser (M * F2)) . F1) + (M . (F2 . (F1 + 1))) is ext-real Element of ExtREAL
f . (F1 + 1) is set
M . (f . (F1 + 1)) is ext-real Element of ExtREAL
((Ser (M * F2)) . F1) + (M . (f . (F1 + 1))) is ext-real Element of ExtREAL
x2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
x2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
s2 . (x2 + 1) is ext-real Element of ExtREAL
s2 . x2 is ext-real Element of ExtREAL
s1 . (x2 + 1) is ext-real Element of ExtREAL
(s2 . x2) + (s1 . (x2 + 1)) is ext-real Element of ExtREAL
x2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
(Ser (M * F2)) . x2 is ext-real Element of ExtREAL
s2 . x2 is ext-real Element of ExtREAL
x2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
(Ser (M * F2)) . (x2 + 1) is ext-real Element of ExtREAL
s2 . (x2 + 1) is ext-real Element of ExtREAL
s1 . (x2 + 1) is ext-real Element of ExtREAL
(s2 . x2) + (s1 . (x2 + 1)) is ext-real Element of ExtREAL
(Ser (M * F2)) . (len s1) is ext-real Element of ExtREAL
x2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
(Ser (M * F2)) . x2 is ext-real Element of ExtREAL
x2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
(Ser (M * F2)) . (x2 + 1) is ext-real Element of ExtREAL
F1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
F1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
Seg (len s1) is finite len s1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
dom s1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
a2 . (F1 + 1) is ext-real Element of ExtREAL
F2 . (F1 + 1) is Element of S
M . (F2 . (F1 + 1)) is ext-real Element of ExtREAL
M . {} is ext-real Element of ExtREAL
(Ser (M * F2)) . (F1 + 1) is ext-real Element of ExtREAL
((Ser (M * F2)) . (len s1)) + (a2 . (F1 + 1)) is ext-real Element of ExtREAL
F1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
F1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
F1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
F1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
x2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
(len s1) - x2 is V36() real ext-real Element of REAL
(Ser (M * F2)) . ((len s1) - x2) is ext-real Element of ExtREAL
x2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
(len s1) - (x2 + 1) is V36() real ext-real Element of REAL
(Ser (M * F2)) . ((len s1) - (x2 + 1)) is ext-real Element of ExtREAL
F1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
(x2 + 1) + F1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
a1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
(Ser (M * F2)) . a1 is ext-real Element of ExtREAL
a1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
(Ser (M * F2)) . (a1 + 1) is ext-real Element of ExtREAL
len f is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
Seg (len f) is finite len f -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
F2 . 0 is Element of S
(Ser (M * F2)) . 0 is ext-real Element of ExtREAL
a2 . 0 is ext-real Element of ExtREAL
M . (F2 . 0) is ext-real Element of ExtREAL
(len s1) - 0 is V36() real ext-real Element of REAL
(Ser (M * F2)) . ((len s1) - 0) is ext-real Element of ExtREAL
x2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
(Ser (M * F2)) . x2 is ext-real Element of ExtREAL
(len s1) + x2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
F1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
x2 + F1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
a1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
(len s1) - x2 is V36() real ext-real Element of REAL
(len s1) - a1 is V36() real ext-real V69() V70() Element of INT
(Ser (M * F2)) . ((len s1) - a1) is ext-real Element of ExtREAL
rng (Ser (M * F2)) is non empty V61() V82() Element of bool ExtREAL
x2 is ext-real set
dom (Ser (M * F2)) is non empty V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
F1 is set
(Ser (M * F2)) . F1 is ext-real Element of ExtREAL
a1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
a1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
a1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
a1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
dom (Ser (M * F2)) is non empty V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
sup (rng (Ser (M * F2))) is ext-real Element of ExtREAL
SUM (M * F2) is ext-real Element of ExtREAL
X is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
dom X is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
S is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
dom S is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum S is ext-real Element of ExtREAL
Sum X is ext-real Element of ExtREAL
M is ext-real Element of ExtREAL
M * (Sum X) is ext-real Element of ExtREAL
len S is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
f is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) V72() Element of bool [:NAT,ExtREAL:]
f . (len S) is ext-real Element of ExtREAL
f . 0 is ext-real Element of ExtREAL
len X is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
s1 is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) V72() Element of bool [:NAT,ExtREAL:]
s1 . (len X) is ext-real Element of ExtREAL
s1 . 0 is ext-real Element of ExtREAL
s2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
f . s2 is ext-real Element of ExtREAL
s1 . s2 is ext-real Element of ExtREAL
M * (s1 . s2) is ext-real Element of ExtREAL
s2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
f . (s2 + 1) is ext-real Element of ExtREAL
s1 . (s2 + 1) is ext-real Element of ExtREAL
M * (s1 . (s2 + 1)) is ext-real Element of ExtREAL
F2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
F2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
Seg (len X) is finite len X -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
f . (F2 + 1) is ext-real Element of ExtREAL
f . F2 is ext-real Element of ExtREAL
S . (F2 + 1) is ext-real Element of ExtREAL
(f . F2) + (S . (F2 + 1)) is ext-real Element of ExtREAL
s1 . F2 is ext-real Element of ExtREAL
M * (s1 . F2) is ext-real Element of ExtREAL
X . (F2 + 1) is ext-real Element of ExtREAL
M * (X . (F2 + 1)) is ext-real Element of ExtREAL
(M * (s1 . F2)) + (M * (X . (F2 + 1))) is ext-real Element of ExtREAL
(s1 . F2) + (X . (F2 + 1)) is ext-real Element of ExtREAL
M * ((s1 . F2) + (X . (F2 + 1))) is ext-real Element of ExtREAL
a2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
s1 . a2 is ext-real Element of ExtREAL
a2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
s1 . (a2 + 1) is ext-real Element of ExtREAL
x2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
x2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
X . (x2 + 1) is ext-real Element of ExtREAL
s1 . (x2 + 1) is ext-real Element of ExtREAL
s1 . x2 is ext-real Element of ExtREAL
(s1 . x2) + (X . (x2 + 1)) is ext-real Element of ExtREAL
(s1 . F2) + (X . (F2 + 1)) is ext-real Element of ExtREAL
M * ((s1 . F2) + (X . (F2 + 1))) is ext-real Element of ExtREAL
a2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
s1 . a2 is ext-real Element of ExtREAL
a2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
s1 . (a2 + 1) is ext-real Element of ExtREAL
x2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
x2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
X . (x2 + 1) is ext-real Element of ExtREAL
s1 . (x2 + 1) is ext-real Element of ExtREAL
s1 . x2 is ext-real Element of ExtREAL
(s1 . x2) + (X . (x2 + 1)) is ext-real Element of ExtREAL
(s1 . F2) + (X . (F2 + 1)) is ext-real Element of ExtREAL
M * ((s1 . F2) + (X . (F2 + 1))) is ext-real Element of ExtREAL
a2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
X . a2 is ext-real Element of ExtREAL
x2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
X . x2 is ext-real Element of ExtREAL
M * (s1 . 0) is ext-real Element of ExtREAL
Seg (len X) is finite len X -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Seg (len S) is finite len S -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
s1 . (len S) is ext-real Element of ExtREAL
M * (s1 . (len S)) is ext-real Element of ExtREAL
X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
rng X is finite V61() V81() V82() V83() Element of bool REAL
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is Relation-like non empty V72() set
bool [:X,ExtREAL:] is non empty set
S is non empty V24() V25() V26() compl-closed sigma-multiplicative sigma-additive Element of bool (bool X)
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is Relation-like non empty V72() set
bool [:X,ExtREAL:] is non empty set
S is non empty V24() V25() V26() compl-closed sigma-multiplicative sigma-additive Element of bool (bool X)
M is Relation-like X -defined ExtREAL -valued Function-like V72() Element of bool [:X,ExtREAL:]
dom M is Element of bool X
f is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng f is finite V61() Element of bool S
bool S is non empty set
union (rng f) is set
dom f is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
s1 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
dom s1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
S is non empty V24() V25() V26() compl-closed sigma-multiplicative sigma-additive Element of bool (bool X)
M is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng M is finite V61() Element of bool S
bool S is non empty set
union (rng M) is set
dom M is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
f is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
s1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
len s1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
rng s1 is finite V61() Element of bool S
union (rng s1) is set
dom s1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
s2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
Seg s2 is finite s2 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
s1 | (Seg s2) is Relation-like NAT -defined Seg s2 -defined NAT -defined S -valued Function-like finite FinSubsequence-like V61() Element of bool [:NAT,S:]
[:NAT,S:] is Relation-like non empty non trivial non finite set
bool [:NAT,S:] is non empty non trivial non finite set
F2 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
len F2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85() V86() Element of NAT
rng F2 is finite V61() Element of bool S
union (rng F2) is set
dom F2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
a2 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng a2 is finite V61() Element of bool S
union (rng a2) is set
dom a2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
s2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive non negative finite cardinal V61() V69() V70() V81() V82() V83() V84() V85()