:: 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() V86() Element of NAT
s1 . (s2 + 1) is set
<*(s1 . (s2 + 1))*> is Relation-like NAT -defined Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V61() set
F2 ^ <*(s1 . (s2 + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like V61() set
dom (F2 ^ <*(s1 . (s2 + 1))*>) is non empty finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
len <*(s1 . (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
(len F2) + (len <*(s1 . (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
Seg ((len F2) + (len <*(s1 . (s2 + 1))*>)) is non empty finite (len F2) + (len <*(s1 . (s2 + 1))*>) -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Seg (s2 + 1) is non empty finite s2 + 1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
s1 . x2 is set
(F2 ^ <*(s1 . (s2 + 1))*>) . x2 is set
s1 | s2 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() FinSequence of S
(s1 | s2) . x2 is set
F2 . x2 is set
dom <*(s1 . (s2 + 1))*> is non empty trivial finite 1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
(len 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
(F2 ^ <*(s1 . (s2 + 1))*>) . ((len F2) + 1) is set
<*(s1 . (s2 + 1))*> . 1 is set
rng <*(s1 . (s2 + 1))*> is non empty trivial finite 1 -element V61() set
{{}} is non empty trivial finite 1 -element V61() set
x2 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
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
x2 . F1 is set
a1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F2 . a1 is set
s1 . a1 is set
(rng F2) \/ (rng <*(s1 . (s2 + 1))*>) is finite V61() set
union (rng <*(s1 . (s2 + 1))*>) is set
(union (rng F2)) \/ (union (rng <*(s1 . (s2 + 1))*>)) is set
(union (rng F2)) \/ {} is set
rng x2 is finite V61() Element of bool S
union (rng x2) is set
a2 ^ <*(s1 . (s2 + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like V61() set
x2 is set
F1 is set
(a2 ^ <*(s1 . (s2 + 1))*>) . x2 is set
(a2 ^ <*(s1 . (s2 + 1))*>) . F1 is set
dom (a2 ^ <*(s1 . (s2 + 1))*>) is non empty finite V61() V81() V82() V83() V84() V85() V86() Element of bool 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 (a2 ^ <*(s1 . (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
len 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
len <*(s1 . (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
(len a2) + (len <*(s1 . (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
(len 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
(a2 ^ <*(s1 . (s2 + 1))*>) . a1 is set
<*(s1 . (s2 + 1))*> . 1 is set
x1 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 (a2 ^ <*(s1 . (s2 + 1))*>)) is non empty finite len (a2 ^ <*(s1 . (s2 + 1))*>) -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Seg ((len a2) + (len <*(s1 . (s2 + 1))*>)) is non empty finite (len a2) + (len <*(s1 . (s2 + 1))*>) -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Seg ((len a2) + 1) is non empty finite (len a2) + 1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
a2 . x1 is set
m is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F2 . m is set
Seg (len F2) is finite len F2 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
(a2 ^ <*(s1 . (s2 + 1))*>) . x1 is set
s1 . m is set
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 (a2 ^ <*(s1 . (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
len 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
len <*(s1 . (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
(len a2) + (len <*(s1 . (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
(len 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
Seg (len (a2 ^ <*(s1 . (s2 + 1))*>)) is non empty finite len (a2 ^ <*(s1 . (s2 + 1))*>) -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Seg ((len a2) + (len <*(s1 . (s2 + 1))*>)) is non empty finite (len a2) + (len <*(s1 . (s2 + 1))*>) -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Seg ((len a2) + 1) is non empty finite (len a2) + 1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
(a2 ^ <*(s1 . (s2 + 1))*>) . a1 is set
a2 . a1 is set
x1 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 ^ <*(s1 . (s2 + 1))*>) . x1 is set
<*(s1 . (s2 + 1))*> . 1 is set
m is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F2 . m is set
Seg (len F2) is finite len F2 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
s1 . m is set
x1 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 ^ <*(s1 . (s2 + 1))*>) . x1 is set
a2 . x1 is set
x1 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
x1 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 (a2 ^ <*(s1 . (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
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 (a2 ^ <*(s1 . (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
dom (a2 ^ <*(s1 . (s2 + 1))*>) is non empty finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
dom (a2 ^ <*(s1 . (s2 + 1))*>) is non empty finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
dom (a2 ^ <*(s1 . (s2 + 1))*>) is non empty finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Seg (s2 + 1) is non empty finite s2 + 1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x2 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
len 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
len 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
len <*(s1 . (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
(len a2) + (len <*(s1 . (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
(len 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
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
x2 . F1 is set
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 <*(s1 . (s2 + 1))*> is non empty trivial finite 1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x2 . a1 is set
<*(s1 . (s2 + 1))*> . 1 is set
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
x2 . a1 is set
a2 . a1 is set
x1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F2 . x1 is set
s1 . x1 is set
x1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
s1 . x1 is set
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
x1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
s1 . x1 is set
m is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
s1 . m is set
rng <*(s1 . (s2 + 1))*> is non empty trivial finite 1 -element V61() set
(rng F2) \/ (rng <*(s1 . (s2 + 1))*>) is finite V61() set
union (rng <*(s1 . (s2 + 1))*>) is set
(union (rng F2)) \/ (union (rng <*(s1 . (s2 + 1))*>)) is set
(rng a2) \/ (rng <*(s1 . (s2 + 1))*>) is finite V61() set
union ((rng a2) \/ (rng <*(s1 . (s2 + 1))*>)) is set
F1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng F1 is finite V61() Element of bool S
union (rng F1) is set
F1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng F1 is finite V61() Element of bool S
union (rng F1) is set
dom F1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng x1 is finite V61() Element of bool S
union (rng x1) is set
dom x1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x2 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng x2 is finite V61() Element of bool S
union (rng x2) is set
dom x2 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
f is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
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
rng f is finite V61() Element of bool S
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 S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
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() set
s1 . s2 is set
X is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence 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
dom X is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum X is ext-real Element of ExtREAL
M is ext-real Element of ExtREAL
S is ext-real Element of ExtREAL
M * S is ext-real Element of ExtREAL
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 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 + 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 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
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
dom s2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum s2 is ext-real Element of ExtREAL
F2 is ext-real Element of ExtREAL
a2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V61() set
x2 is set
<*x2*> is Relation-like NAT -defined Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V61() set
a2 ^ <*x2*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like V61() set
F1 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
len 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
len <*x2*> 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 F1) + (len <*x2*>) 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 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
dom <*x2*> is non empty trivial finite 1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
<*x2*> . 1 is set
s2 . (s1 + 1) is ext-real Element of ExtREAL
Sum F1 is ext-real Element of ExtREAL
x1 is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) V72() Element of bool [:NAT,ExtREAL:]
x1 . (len F1) is ext-real Element of ExtREAL
x1 . 0 is ext-real Element of ExtREAL
dom F1 is finite 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
F1 . m is ext-real Element of ExtREAL
a1 is ext-real Element of ExtREAL
<*a1*> 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
len <*a1*> 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 F1) + (len <*a1*>) 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 . m is ext-real Element of ExtREAL
m is ext-real Element of ExtREAL
m * F2 is ext-real Element of ExtREAL
n is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) V72() Element of bool [:NAT,ExtREAL:]
n . (len s2) is ext-real Element of ExtREAL
n . 0 is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
n . a is ext-real Element of ExtREAL
x1 . a is ext-real Element of ExtREAL
a + 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
n . (a + 1) is ext-real Element of ExtREAL
x1 . (a + 1) is ext-real Element of ExtREAL
p 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
p + 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
a1 is ext-real Element of ExtREAL
<*a1*> 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
len <*a1*> 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 F1) + (len <*a1*>) 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
n . (p + 1) is ext-real Element of ExtREAL
n . p is ext-real Element of ExtREAL
s2 . (p + 1) is ext-real Element of ExtREAL
(n . p) + (s2 . (p + 1)) is ext-real Element of ExtREAL
x1 . (p + 1) is ext-real Element of ExtREAL
x1 . p is ext-real Element of ExtREAL
F1 . (p + 1) is ext-real Element of ExtREAL
(x1 . p) + (F1 . (p + 1)) is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
n . a is ext-real Element of ExtREAL
x1 . a is ext-real Element of ExtREAL
1. is ext-real Element of ExtREAL
m + 1. is ext-real Element of ExtREAL
(m + 1.) * F2 is ext-real Element of ExtREAL
n . s1 is ext-real Element of ExtREAL
(n . s1) + (s2 . (s1 + 1)) is ext-real Element of ExtREAL
x1 . s1 is ext-real Element of ExtREAL
(x1 . s1) + (s2 . (s1 + 1)) is ext-real Element of ExtREAL
(Sum F1) + F2 is ext-real Element of ExtREAL
1. * F2 is ext-real Element of ExtREAL
(m * F2) + (1. * F2) is ext-real Element of ExtREAL
s2 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
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
dom s2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
F2 is ext-real Element of ExtREAL
Sum s2 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
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
dom f is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum f is ext-real Element of ExtREAL
s1 is ext-real Element of ExtREAL
0. * s1 is ext-real Element of ExtREAL
s2 is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) V72() Element of bool [:NAT,ExtREAL:]
s2 . (len f) is ext-real Element of ExtREAL
s2 . 0 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
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
dom f is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
s1 is ext-real Element of ExtREAL
Sum f is ext-real Element of ExtREAL
f is ext-real Element of ExtREAL
f * S is ext-real Element of ExtREAL
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 S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
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
<*{}*> is Relation-like NAT -defined Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V61() set
<*{}*> ^ s1 is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like V61() set
rng <*{}*> is non empty trivial finite 1 -element V61() set
{{}} is non empty trivial finite 1 -element V61() set
(rng <*{}*>) \/ (rng s1) is finite V61() set
rng (<*{}*> ^ s1) is non empty finite V61() set
F2 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() FinSequence of S
a2 is set
x2 is set
F2 . a2 is set
F2 . x2 is set
dom F2 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
len (<*{}*> ^ s1) 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 non empty finite len (<*{}*> ^ s1) -element V61() V81() V82() V83() V84() V85() V86() Element of bool 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 <*{}*> is non empty trivial finite 1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
F2 . F1 is set
<*{}*> . F1 is set
F2 . a1 is set
<*{}*> . a1 is set
len <*{}*> 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
F2 . a1 is set
a1 - (len <*{}*>) is V36() real ext-real V69() V70() Element of INT
s1 . (a1 - (len <*{}*>)) is set
F2 . F1 is set
F1 - (len <*{}*>) is V36() real ext-real V69() V70() Element of INT
s1 . (F1 - (len <*{}*>)) is set
dom F2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
dom F2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
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
union ((rng <*{}*>) \/ (rng s1)) is set
{{}} \/ (rng s1) is finite V61() set
union ({{}} \/ (rng s1)) is set
union {{}} is set
(union {{}}) \/ (union (rng s1)) is set
{} \/ (union (rng s1)) is set
dom a2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
len 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
Seg (len a2) is finite len a2 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
a2 . x2 is set
F1 is ext-real Element of ExtREAL
x1 is Element of X
M . x1 is ext-real Element of ExtREAL
len <*{}*> 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 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 <*{}*>) + (len s1) 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
x2 - (len <*{}*>) is V36() real ext-real Element of REAL
1 + 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 <*{}*>) + 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() set
((len <*{}*>) + 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
1 + a1 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
s1 . (1 + a1) is set
x1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
f . x1 is set
s1 . (x2 - (len <*{}*>)) is set
m is set
M . m is ext-real Element of ExtREAL
n is ext-real Element of ExtREAL
p is Element of X
M . p is ext-real Element of ExtREAL
a is Element of X
a1 is ext-real Element of ExtREAL
m is ext-real Element of ExtREAL
F1 is ext-real Element of ExtREAL
x2 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
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
a2 . F1 is set
x2 . F1 is ext-real Element of ExtREAL
a1 is Element of X
M . a1 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 . F1 is ext-real Element of ExtREAL
1 + 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 <*{}*> 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 <*{}*>) + 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 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 <*{}*>) + (len s1) 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
a2 . F1 is set
F1 - (len <*{}*>) is V36() real ext-real Element of REAL
s1 . (F1 - (len <*{}*>)) is set
F1 - 1 is V36() real ext-real Element of REAL
s1 . (F1 - 1) is set
dom <*{}*> is non empty trivial finite 1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
a1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
(len <*{}*>) + a1 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 + a1 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
x1 is set
m is Element of X
M . m is ext-real Element of ExtREAL
|.(M . m).| is ext-real Element of ExtREAL
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
a2 . F1 is set
x2 . F1 is ext-real Element of ExtREAL
a1 is set
M . a1 is ext-real Element of ExtREAL
dom <*{}*> is non empty trivial finite 1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
a2 . 1 is set
<*{}*> . 1 is set
1 + 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
a1 is set
M . a1 is ext-real Element of ExtREAL
x1 is Element of X
M . x1 is ext-real Element of ExtREAL
a1 is set
M . a1 is ext-real Element of ExtREAL
len <*{}*> 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 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 <*{}*>) + (len s1) 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 + (len s1) 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() set
x2 . F1 is ext-real Element of ExtREAL
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 set
M . f is ext-real Element of ExtREAL
f is set
M . f is ext-real Element of ExtREAL
s2 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng s2 is finite V61() Element of bool S
bool S is non empty set
union (rng s2) is set
dom s2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
s1 is Element of X
F2 is set
a2 is set
s2 . a2 is set
{ b₁ where b₁ is Element of S : ( b₁ in rng s2 & ( for b₂ being Element of X holds
( not b₂ in b₁ or M . b₂ = 0. ) ) ) } is set
union { b₁ where b₁ is Element of S : ( b₁ in rng s2 & ( for b₂ being Element of X holds
( not b₂ in b₁ or M . b₂ = 0. ) ) ) } is set
bool X is non empty Element of bool (bool X)
a1 is set
x1 is Element of S
{ 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 : ( b₁ in dom s2 & ( for b₂ being Element of X holds
( not b₂ in s2 . b₁ or M . b₂ = 0. ) ) ) } is set
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
(len 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
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
s2 . m is set
n is Element of X
M . n is ext-real Element of ExtREAL
a1 is Element of bool (bool X)
n is set
a is Element of S
n is set
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
s2 . a is set
n is finite V61() set
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V61() set
rng a is finite V61() set
p is non empty V61() Element of bool (bool X)
q is set
k is Element of S
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
card n 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 omega
Seg (len s2) is finite len s2 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
findom s2 is finite V61() Element of K101(NAT)
(findom s2) \ n is finite V61() Element of bool (findom s2)
bool (findom s2) is non empty finite V47() V61() set
ss is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V61() set
rng ss is finite V61() set
k is finite V61() set
card k 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 omega
F21 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
(len a) + F21 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 s2)) \ n is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
card ((findom s2) \ n) 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 omega
card (Seg (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 omega
(card (Seg (len s2))) - (card n) is V36() real ext-real V69() V70() Element of INT
q is Element of S
len ss 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 s2) - (len a) is V36() real ext-real V69() V70() Element of INT
((len s2) - (len a)) + 1 is V36() real ext-real V69() V70() Element of INT
(((len s2) - (len a)) + 1) - 1 is V36() real ext-real V69() V70() Element of INT
j 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 j is finite j -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
x - 1 is V36() real ext-real Element of REAL
c₂₄ is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
1 + c₂₄ 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 + 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
j - 1 is V36() real ext-real V69() V70() Element of INT
Seg (len ss) is finite len ss -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
dom ss is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
ss . c₂₄ is set
s2 . (ss . c₂₄) is set
F is Element of S
x is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() FinSequence of S
dom x is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
1. 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
Seg (len x) is finite len x -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
c₂₄ is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
x . c₂₄ is set
n is Element of X
M . n is ext-real Element of ExtREAL
k1 is set
Fn is Element of S
1 + 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
c₂₄ - 1 is V36() real ext-real Element of REAL
F is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
ss . F is set
s2 . (ss . F) is set
Seg (len ss) is finite len ss -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
dom ss is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
n is set
s2 . n is set
Fn is Element of X
M . Fn is ext-real Element of ExtREAL
k1 is set
rng x is finite V61() Element of bool S
Fn is Element of X
M . Fn is ext-real Element of ExtREAL
y is ext-real Element of ExtREAL
y is Element of X
M . y is ext-real Element of ExtREAL
Fn is ext-real Element of ExtREAL
y is ext-real Element of ExtREAL
n is ext-real Element of ExtREAL
k1 is ext-real Element of ExtREAL
c₂₄ is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
dom c₂₄ 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
x . F is set
c₂₄ . F is ext-real Element of ExtREAL
n is Element of X
M . n is ext-real Element of ExtREAL
F is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
x . F is set
c₂₄ . F is ext-real Element of ExtREAL
n is set
M . n is ext-real Element of ExtREAL
rng x is finite V61() Element of bool S
k1 is Element of X
M . k1 is ext-real Element of ExtREAL
F is Element of X
M . F is ext-real Element of ExtREAL
c₂₄ . 1 is ext-real Element of ExtREAL
0 + 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 . 1 is set
F is Element of S
n is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
k1 is Element of X
x . n is set
c₂₄ . n is ext-real Element of ExtREAL
M . k1 is ext-real Element of ExtREAL
F is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
n is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
x . F is set
x . n is set
n - 1 is V36() real ext-real Element of REAL
j - 1 is V36() real ext-real V69() V70() Element of INT
1 + 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
k1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
ss . k1 is set
s2 . (ss . k1) is set
Seg (len ss) is finite len ss -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
dom ss is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
(x . F) /\ (x . n) is set
Fn is set
y is set
y is Element of S
m2 is set
s2 . m2 is set
n9 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 . n9 is set
(s2 . n9) /\ (s2 . (ss . k1)) is set
F is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
n is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
x . F is set
x . n is set
F - 1 is V36() real ext-real Element of REAL
j - 1 is V36() real ext-real V69() V70() Element of INT
n - 1 is V36() real ext-real Element of REAL
1 + 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
k1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
ss . k1 is set
s2 . (ss . k1) is set
Seg (len ss) is finite len ss -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
dom ss is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Fn is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
ss . Fn is set
s2 . (ss . Fn) is set
F is set
n is set
x . F is set
x . n is set
k1 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
Fn 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
k1 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
Fn 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
k1 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
Fn 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
k1 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
Fn 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 x is finite V61() Element of bool S
union (rng x) is set
F is set
n is set
k1 is set
x . k1 is set
Fn 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
y is set
y is Element of S
Fn 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 + 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
Fn - 1 is V36() real ext-real V69() V70() Element of INT
x . Fn is set
y is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
ss . y is set
s2 . (ss . y) is set
dom ss is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Fn 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
Fn 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 set
n is set
k1 is set
s2 . k1 is set
Fn 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
y 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 . y is set
union p is Element of bool X
1 + 0 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 . 1 is set
Fn 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 ss is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
y is set
ss . y is set
y 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 ss) is finite len ss -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
y + 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 + 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
m2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
x . m2 is set
m2 - 1 is V36() real ext-real Element of REAL
n9 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
ss . n9 is set
s2 . (ss . n9) is set
Fn 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
Fn 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 S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
0 + 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
dom F is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
n is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
c₂₄ . n is ext-real Element of ExtREAL
1 + 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
n - 1 is V36() real ext-real Element of REAL
F . n is set
k1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
ss . k1 is set
s2 . (ss . k1) is set
j - 1 is V36() real ext-real V69() V70() Element of INT
Seg (len ss) is finite len ss -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
dom ss is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
F . 1 is set
rng F is finite V61() Element of bool S
y is set
y is Element of X
M . y is ext-real Element of ExtREAL
q /\ (F . n) is Element of bool X
m2 is Element of X
M . m2 is ext-real Element of ExtREAL
Fn is Element of S
union (rng F) is set
|.(M . y).| is ext-real Element of ExtREAL
x . n is set
Fn is Element of X
M . Fn is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
c₂₄ . n is ext-real Element of ExtREAL
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 set
M . f is ext-real Element of ExtREAL
f is set
M . f is ext-real Element of ExtREAL
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
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 Element of X
M . s2 is ext-real Element of ExtREAL
dom f is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
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
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
Seg (len s1) is finite len s1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
rng f is finite V61() Element of bool S
bool S is non empty set
union (rng f) is set
Sum F2 is ext-real Element of ExtREAL
a2 is set
x2 is set
f . x2 is set
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
Seg (len F2) is finite len F2 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
a1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F2 . a1 is ext-real Element of ExtREAL
f . a1 is set
f . F1 is set
(f . a1) /\ (f . F1) is set
chi ((f . a1),X) is Relation-like X -defined ExtREAL -valued Function-like V72() Element of bool [:X,ExtREAL:]
(chi ((f . a1),X)) . s2 is ext-real Element of ExtREAL
s1 . a1 is ext-real Element of ExtREAL
(s1 . a1) * ((chi ((f . a1),X)) . s2) is ext-real Element of ExtREAL
a1 is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) V72() Element of bool [:NAT,ExtREAL:]
a1 . (len F2) is ext-real Element of ExtREAL
a1 . 0 is ext-real Element of ExtREAL
x1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F2 . x1 is ext-real Element of ExtREAL
f . x1 is set
chi ((f . x1),X) is Relation-like X -defined ExtREAL -valued Function-like V72() Element of bool [:X,ExtREAL:]
(chi ((f . x1),X)) . s2 is ext-real Element of ExtREAL
1. is ext-real Element of ExtREAL
s1 . x1 is ext-real Element of ExtREAL
(s1 . x1) * 1. is ext-real Element of ExtREAL
x1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
a1 . x1 is ext-real Element of ExtREAL
x1 + 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
a1 . (x1 + 1) is ext-real Element of ExtREAL
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
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
a1 . (m + 1) is ext-real Element of ExtREAL
F2 . (m + 1) is ext-real Element of ExtREAL
0. + (F2 . (m + 1)) is ext-real Element of ExtREAL
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
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
a1 . (m + 1) is ext-real Element of ExtREAL
a1 . m is ext-real Element of ExtREAL
F2 . (m + 1) is ext-real Element of ExtREAL
(a1 . m) + (F2 . (m + 1)) is ext-real Element of ExtREAL
F2 . F1 is ext-real Element of ExtREAL
a1 . (m + 1) is ext-real Element of ExtREAL
a1 . m is ext-real Element of ExtREAL
F2 . (m + 1) is ext-real Element of ExtREAL
(a1 . m) + (F2 . (m + 1)) is ext-real Element of ExtREAL
(M . s2) + 0. is ext-real Element of ExtREAL
a1 . (m + 1) is ext-real Element of ExtREAL
a1 . (m + 1) is ext-real Element of ExtREAL
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
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
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
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
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
X is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence 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 X is ext-real Element of ExtREAL
Sum S 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
rng X is finite V61() V82() Element of bool ExtREAL
Sum X is ext-real Element of ExtREAL
dom X is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
S is set
X . S is ext-real Element of ExtREAL
S is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
X . S 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
Seg (len X) is finite len X -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
M is Relation-like NAT -defined ExtREAL -valued Function-like non empty total V18( NAT , ExtREAL ) V72() Element of bool [:NAT,ExtREAL:]
M . (len X) is ext-real Element of ExtREAL
M . 0 is ext-real Element of ExtREAL
f is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
X . f is ext-real Element of ExtREAL
f is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
M . f is ext-real Element of ExtREAL
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
M . (f + 1) is ext-real Element of ExtREAL
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
s1 + 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 . (s1 + 1) is ext-real Element of ExtREAL
-infty + -infty is non empty non real ext-real non positive negative Element of ExtREAL
M . s1 is ext-real Element of ExtREAL
(M . s1) + (X . (s1 + 1)) is ext-real Element of ExtREAL
M . (s1 + 1) is ext-real Element of ExtREAL
s1 + 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
M . (s1 + 1) is ext-real Element of ExtREAL
M . s1 is ext-real Element of ExtREAL
X . (s1 + 1) is ext-real Element of ExtREAL
(M . s1) + (X . (s1 + 1)) is ext-real Element of ExtREAL
M . (s1 + 1) is ext-real Element of ExtREAL
M . s1 is ext-real Element of ExtREAL
X . (s1 + 1) is ext-real Element of ExtREAL
(M . s1) + (X . (s1 + 1)) is ext-real Element of ExtREAL
M . (s1 + 1) is ext-real Element of ExtREAL
M . (s1 + 1) is ext-real Element of ExtREAL
s1 + 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
M . (s1 + 1) is ext-real Element of ExtREAL
s1 + 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
M . (s1 + 1) is ext-real Element of ExtREAL
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
[:X,ExtREAL:] is Relation-like non empty V72() set
bool [:X,ExtREAL:] is non empty set
f is Relation-like X -defined ExtREAL -valued Function-like V72() Element of bool [:X,ExtREAL:]
dom f is Element of bool X
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:]
s1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
s2 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
s2 . 1 is ext-real Element of ExtREAL
dom s2 is finite 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
M * s1 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
F2 is set
s2 . F2 is ext-real Element of ExtREAL
(M * s1) . F2 is ext-real Element of ExtREAL
(s2 . F2) * ((M * s1) . F2) is ext-real Element of ExtREAL
F2 is Relation-like NAT -defined ExtREAL -valued Function-like V72() Element of bool [:NAT,ExtREAL:]
dom F2 is V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
a2 is set
a2 is set
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
Seg (len s1) is finite len s1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
rng F2 is V82() Element of bool ExtREAL
a2 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
Sum a2 is ext-real Element of ExtREAL
dom a2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
a2 . x2 is ext-real Element of ExtREAL
s2 . x2 is ext-real Element of ExtREAL
(M * s1) . x2 is ext-real Element of ExtREAL
(s2 . x2) * ((M * s1) . x2) is ext-real Element of ExtREAL
s1 is ext-real Element of ExtREAL
s2 is ext-real Element of ExtREAL
F2 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
a2 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
a2 . 1 is ext-real Element of ExtREAL
dom a2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x2 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
dom x2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
dom F2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
M * F2 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
Sum x2 is ext-real Element of ExtREAL
F2 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
a2 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
a2 . 1 is ext-real Element of ExtREAL
dom a2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x2 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
dom x2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
dom F2 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
M * F2 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
Sum x2 is ext-real Element of ExtREAL
F1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
a2 . F1 is ext-real Element of ExtREAL
len 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
Seg (len a2) is finite len a2 -element V61() V81() V82() V83() V84() V85() V86() Element of bool 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
1 + 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() set
(M * F2) . F1 is ext-real Element of ExtREAL
F2 . F1 is set
M . (F2 . F1) is ext-real Element of ExtREAL
rng F2 is finite V61() Element of bool S
bool S is non empty set
rng x2 is finite V61() V82() Element of bool ExtREAL
F1 is set
x2 . F1 is ext-real Element of ExtREAL
a2 . F1 is ext-real Element of ExtREAL
(M * F2) . F1 is ext-real Element of ExtREAL
(a2 . F1) * ((M * F2) . F1) is ext-real Element of ExtREAL
F1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
a1 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
a1 . 1 is ext-real Element of ExtREAL
dom a1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x1 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
dom x1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
dom F1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
M * F1 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
Sum x1 is ext-real Element of ExtREAL
F1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
a1 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
a1 . 1 is ext-real Element of ExtREAL
dom a1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x1 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
dom x1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
dom F1 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
M * F1 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
Sum x1 is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
a1 . m is ext-real Element of ExtREAL
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
Seg (len a1) is finite len a1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
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
1 + 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
m is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
(M * F1) . m is ext-real Element of ExtREAL
F1 . m is set
M . (F1 . m) is ext-real Element of ExtREAL
rng F1 is finite V61() Element of bool S
bool S is non empty set
rng x1 is finite V61() V82() Element of bool ExtREAL
m is set
x1 . m is ext-real Element of ExtREAL
a1 . m is ext-real Element of ExtREAL
(M * F1) . m is ext-real Element of ExtREAL
(a1 . m) * ((M * F1) . m) is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
n is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F1 . m is set
F2 . n is set
(F1 . m) /\ (F2 . n) is set
M . ((F1 . m) /\ (F2 . n)) is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
n is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F1 . m is set
F2 . n is set
(F1 . m) /\ (F2 . n) is set
M . ((F1 . m) /\ (F2 . n)) is ext-real Element of ExtREAL
rng F2 is finite V61() Element of bool S
bool S is non empty set
rng F1 is finite V61() Element of bool S
M . (F1 . m) is ext-real Element of ExtREAL
(M * F1) . m is ext-real Element of ExtREAL
a1 . m is ext-real Element of ExtREAL
(a1 . m) * ((M * F1) . m) is ext-real Element of ExtREAL
x1 . m is ext-real Element of ExtREAL
M . (F2 . n) is ext-real Element of ExtREAL
(M * F2) . n is ext-real Element of ExtREAL
a2 . n is ext-real Element of ExtREAL
(a2 . n) * ((M * F2) . n) is ext-real Element of ExtREAL
x2 . n is ext-real Element of ExtREAL
len 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
len x1 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 x1) is finite len x1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Seg (len x2) is finite len x2 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
[:(Seg (len x1)),(Seg (len x2)):] is Relation-like RAT -valued INT -valued finite V61() V71() V72() V73() V74() set
[:[:(Seg (len x1)),(Seg (len x2)):],REAL:] is Relation-like V71() V72() V73() set
bool [:[:(Seg (len x1)),(Seg (len x2)):],REAL:] is non empty set
a is set
p is set
a1 . a is ext-real Element of ExtREAL
F1 . a is set
F2 . p is set
(F1 . a) /\ (F2 . p) is set
M . ((F1 . a) /\ (F2 . p)) is ext-real Element of ExtREAL
(a1 . a) * (M . ((F1 . a) /\ (F2 . p))) is ext-real Element of ExtREAL
{ 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₁ <= len x1 ) } is set
q 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₁ <= len x2 ) } is set
k 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 . k is set
rng F2 is finite V61() Element of bool S
bool S is non empty set
F1 . q is set
rng F1 is finite V61() Element of bool S
(F1 . q) /\ (F2 . k) is set
1 + 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
a1 . q is ext-real Element of ExtREAL
M . ((F1 . q) /\ (F2 . k)) is ext-real Element of ExtREAL
(a1 . q) * (M . ((F1 . q) /\ (F2 . k))) is ext-real Element of ExtREAL
0. * (M . ((F1 . q) /\ (F2 . k))) is ext-real Element of ExtREAL
1 + 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
a1 . q is ext-real Element of ExtREAL
M . ((F1 . q) /\ (F2 . k)) is ext-real Element of ExtREAL
(a1 . q) * (M . ((F1 . q) /\ (F2 . k))) is ext-real Element of ExtREAL
(a1 . q) * 0. is ext-real Element of ExtREAL
s is set
a1 . q is ext-real Element of ExtREAL
f . s is ext-real Element of ExtREAL
a2 . k is ext-real Element of ExtREAL
M . ((F1 . q) /\ (F2 . k)) is ext-real Element of ExtREAL
(a1 . q) * (M . ((F1 . q) /\ (F2 . k))) is ext-real Element of ExtREAL
a1 . q is ext-real Element of ExtREAL
M . ((F1 . q) /\ (F2 . k)) is ext-real Element of ExtREAL
(a1 . q) * (M . ((F1 . q) /\ (F2 . k))) is ext-real Element of ExtREAL
a1 . q is ext-real Element of ExtREAL
M . ((F1 . q) /\ (F2 . k)) is ext-real Element of ExtREAL
(a1 . q) * (M . ((F1 . q) /\ (F2 . k))) is ext-real Element of ExtREAL
a1 . q is ext-real Element of ExtREAL
M . ((F1 . q) /\ (F2 . k)) is ext-real Element of ExtREAL
(a1 . q) * (M . ((F1 . q) /\ (F2 . k))) is ext-real Element of ExtREAL
a1 . q is ext-real Element of ExtREAL
M . ((F1 . q) /\ (F2 . k)) is ext-real Element of ExtREAL
(a1 . q) * (M . ((F1 . q) /\ (F2 . k))) is ext-real Element of ExtREAL
a1 . q is ext-real Element of ExtREAL
M . ((F1 . q) /\ (F2 . k)) is ext-real Element of ExtREAL
(a1 . q) * (M . ((F1 . q) /\ (F2 . k))) is ext-real Element of ExtREAL
s is V36() real ext-real Element of REAL
ss is V36() real ext-real Element of REAL
s * ss is V36() real ext-real Element of REAL
a1 . q is ext-real Element of ExtREAL
M . ((F1 . q) /\ (F2 . k)) is ext-real Element of ExtREAL
(a1 . q) * (M . ((F1 . q) /\ (F2 . k))) is ext-real Element of ExtREAL
a1 . q is ext-real Element of ExtREAL
M . ((F1 . q) /\ (F2 . k)) is ext-real Element of ExtREAL
(a1 . q) * (M . ((F1 . q) /\ (F2 . k))) is ext-real Element of ExtREAL
a is Relation-like [:(Seg (len x1)),(Seg (len x2)):] -defined REAL -valued Function-like total V18([:(Seg (len x1)),(Seg (len x2)):], REAL ) finite V61() V71() V72() V73() Element of bool [:[:(Seg (len x1)),(Seg (len x2)):],REAL:]
p is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
q is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
a . (p,q) is set
[p,q] is set
{p,q} is finite V47() V61() V81() V82() V83() V84() V85() V86() set
{p} is non empty trivial finite V47() 1 -element V61() V81() V82() V83() V84() V85() V86() set
{{p,q},{p}} is finite V47() V61() set
a . [p,q] is V36() real ext-real set
a1 . p is ext-real Element of ExtREAL
F1 . p is set
F2 . q is set
(F1 . p) /\ (F2 . q) is set
M . ((F1 . p) /\ (F2 . q)) is ext-real Element of ExtREAL
(a1 . p) * (M . ((F1 . p) /\ (F2 . q))) is ext-real Element of ExtREAL
a is Relation-like [:(Seg (len x1)),(Seg (len x2)):] -defined REAL -valued Function-like total V18([:(Seg (len x1)),(Seg (len x2)):], REAL ) finite V61() V71() V72() V73() Element of bool [:[:(Seg (len x1)),(Seg (len x2)):],REAL:]
a is Relation-like [:(Seg (len x1)),(Seg (len x2)):] -defined REAL -valued Function-like total V18([:(Seg (len x1)),(Seg (len x2)):], REAL ) finite V61() V71() V72() V73() Element of bool [:[:(Seg (len x1)),(Seg (len x2)):],REAL:]
p is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V61() set
len q 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 q is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
q . k is set
[p,k] is set
{p,k} is finite V47() V61() V81() V82() V83() V84() V85() V86() set
{p} is non empty trivial finite V47() 1 -element V61() V81() V82() V83() V84() V85() V86() set
{{p,k},{p}} is finite V47() V61() set
a . [p,k] is V36() real ext-real Element of REAL
k is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
Sum k is V36() real ext-real Element of REAL
s is V36() real ext-real Element of REAL
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V61() set
dom p is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
q is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
p . q is set
k is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom k is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum k is V36() real ext-real Element of REAL
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
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
p is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom p is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
p is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom p is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
q is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
p . q is V36() real ext-real Element of REAL
x1 . q is ext-real Element of ExtREAL
k is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom k is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum k is V36() real ext-real Element of REAL
F1 . q is set
s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V61() set
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
dom s is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
ss is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
s . ss is set
F2 . ss is set
rng F2 is finite V61() Element of bool S
bool S is non empty set
rng F1 is finite V61() Element of bool S
(F1 . q) /\ (F2 . ss) is set
ss is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() FinSequence of S
dom ss is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
F21 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng F21 is finite V61() Element of bool S
bool S is non empty set
union (rng F21) is set
dom F21 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
rng F2 is finite V61() Element of bool S
union (rng F2) is set
(F1 . q) /\ (union (rng F2)) is set
(F1 . q) /\ (dom f) is Element of bool X
rng F1 is finite V61() Element of bool S
union (rng F1) is set
(F1 . q) /\ (union (rng F1)) is set
j is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F21 . j is set
F2 . j is set
(F1 . q) /\ (F2 . j) is set
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng s is finite V61() Element of bool S
bool S is non empty set
union (rng s) is set
dom s is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng s is finite V61() Element of bool S
bool S is non empty set
union (rng s) is set
dom s is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
M * s is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
Sum (M * s) is ext-real Element of ExtREAL
M . (F1 . q) is ext-real Element of ExtREAL
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
Seg (len a1) is finite len a1 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
a1 . q is ext-real Element of ExtREAL
1 + 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
F21 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
k . F21 is V36() real ext-real Element of REAL
F2 . F21 is set
(F1 . q) /\ (F2 . F21) is set
M . ((F1 . q) /\ (F2 . F21)) is ext-real Element of ExtREAL
(a1 . q) * (M . ((F1 . q) /\ (F2 . F21))) is ext-real Element of ExtREAL
a . (q,F21) is set
[q,F21] is set
{q,F21} is finite V47() V61() V81() V82() V83() V84() V85() V86() set
{q} is non empty trivial finite V47() 1 -element V61() V81() V82() V83() V84() V85() V86() set
{{q,F21},{q}} is finite V47() V61() set
a . [q,F21] is V36() real ext-real set
ss is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
dom ss is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
F21 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
ss . F21 is ext-real Element of ExtREAL
(M * s) . F21 is ext-real Element of ExtREAL
(a1 . q) * ((M * s) . F21) is ext-real Element of ExtREAL
F2 . F21 is set
(F1 . q) /\ (F2 . F21) is set
M . ((F1 . q) /\ (F2 . F21)) is ext-real Element of ExtREAL
(a1 . q) * (M . ((F1 . q) /\ (F2 . F21))) is ext-real Element of ExtREAL
s . F21 is set
M . (s . F21) is ext-real Element of ExtREAL
(a1 . q) * (M . (s . F21)) is ext-real Element of ExtREAL
dom (M * s) is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum ss is ext-real Element of ExtREAL
(a1 . q) * (Sum (M * s)) is ext-real Element of ExtREAL
(a1 . q) * (M . (F1 . q)) is ext-real Element of ExtREAL
(M * F1) . q is ext-real Element of ExtREAL
(a1 . q) * ((M * F1) . q) is ext-real Element of ExtREAL
Sum p is V36() real ext-real Element of REAL
q is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V61() set
len k 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 k is finite 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() set
k . s is set
[s,q] is set
{s,q} is finite V47() V61() V81() V82() V83() V84() V85() V86() set
{s} is non empty trivial finite V47() 1 -element V61() V81() V82() V83() V84() V85() V86() set
{{s,q},{s}} is finite V47() V61() set
a . [s,q] is V36() real ext-real Element of REAL
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
ss is V36() real ext-real Element of REAL
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V61() set
dom q is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
q . k is set
s is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom s is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum s is V36() real ext-real Element of REAL
k is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V71() V72() V73() FinSequence of REAL
dom k is finite 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() set
k . s is V36() real ext-real Element of REAL
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
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
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
x2 . k 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
dom s is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum s is V36() real ext-real Element of REAL
F2 . k is set
F21 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V61() set
len F21 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 F21 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
j is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F21 . j is set
F1 . j is set
rng F1 is finite V61() Element of bool S
bool S is non empty set
rng F2 is finite V61() Element of bool S
(F1 . j) /\ (F2 . k) is set
j is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() FinSequence of S
dom j is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
x is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng x is finite V61() Element of bool S
bool S is non empty set
union (rng x) is set
dom x is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
rng F1 is finite V61() Element of bool S
union (rng F1) is set
(F2 . k) /\ (union (rng F1)) is set
(F2 . k) /\ (dom f) is Element of bool X
rng F2 is finite V61() Element of bool S
union (rng F2) is set
(F2 . k) /\ (union (rng F2)) is set
c₂₄ is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
x . c₂₄ is set
F1 . c₂₄ is set
(F1 . c₂₄) /\ (F2 . k) is set
F21 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng F21 is finite V61() Element of bool S
bool S is non empty set
union (rng F21) is set
dom F21 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
F21 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V61() disjoint_valued FinSequence of S
rng F21 is finite V61() Element of bool S
bool S is non empty set
union (rng F21) is set
dom F21 is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
M * F21 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
Sum (M * F21) is ext-real Element of ExtREAL
M . (F2 . k) is ext-real Element of ExtREAL
j is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
s . j is V36() real ext-real Element of REAL
a1 . j is ext-real Element of ExtREAL
F1 . j is set
(F1 . j) /\ (F2 . k) is set
M . ((F1 . j) /\ (F2 . k)) is ext-real Element of ExtREAL
(a1 . j) * (M . ((F1 . j) /\ (F2 . k))) is ext-real Element of ExtREAL
a . (j,k) is set
[j,k] is set
{j,k} is finite V47() V61() V81() V82() V83() V84() V85() V86() set
{j} is non empty trivial finite V47() 1 -element V61() V81() V82() V83() V84() V85() V86() set
{{j,k},{j}} is finite V47() V61() set
a . [j,k] is V36() real ext-real set
a2 . k is ext-real Element of ExtREAL
j is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
s . j is V36() real ext-real Element of REAL
F1 . j is set
(F1 . j) /\ (F2 . k) is set
M . ((F1 . j) /\ (F2 . k)) is ext-real Element of ExtREAL
(a2 . k) * (M . ((F1 . j) /\ (F2 . k))) is ext-real Element of ExtREAL
a1 . j is ext-real Element of ExtREAL
(a1 . j) * 0. is ext-real Element of ExtREAL
(a2 . k) * 0. is ext-real Element of ExtREAL
x is set
a1 . j is ext-real Element of ExtREAL
f . x is ext-real Element of ExtREAL
ss is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V61() V72() FinSequence of ExtREAL
dom ss is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
j is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
ss . j is ext-real Element of ExtREAL
(M * F21) . j is ext-real Element of ExtREAL
(a2 . k) * ((M * F21) . j) is ext-real Element of ExtREAL
F1 . j is set
(F1 . j) /\ (F2 . k) is set
M . ((F1 . j) /\ (F2 . k)) is ext-real Element of ExtREAL
(a2 . k) * (M . ((F1 . j) /\ (F2 . k))) is ext-real Element of ExtREAL
F21 . j is set
M . (F21 . j) is ext-real Element of ExtREAL
(a2 . k) * (M . (F21 . j)) is ext-real Element of ExtREAL
len 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
Seg (len a2) is finite len a2 -element V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
1 + 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
dom (M * F21) is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
Sum ss is ext-real Element of ExtREAL
(a2 . k) * (Sum (M * F21)) is ext-real Element of ExtREAL
(a2 . k) * (M . (F2 . k)) is ext-real Element of ExtREAL
(M * F2) . k is ext-real Element of ExtREAL
(a2 . k) * ((M * F2) . k) is ext-real Element of ExtREAL
Sum q 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
n is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F1 . m is set
F2 . n is set
(F1 . m) /\ (F2 . n) is set
M . ((F1 . m) /\ (F2 . n)) is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
n is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real non negative finite cardinal V61() set
F1 . m is set
F2 . n is set
(F1 . m) /\ (F2 . n) is set
M . ((F1 . m) /\ (F2 . n)) is ext-real Element of ExtREAL
M 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
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
dom X is finite V61() V81() V82() V83() V84() V85() V86() Element of bool NAT
S is ext-real Element of ExtREAL
Sum X is ext-real Element of ExtREAL
M * S is ext-real Element of ExtREAL