:: EXTREAL1 semantic presentation

REAL is non empty V12() V36() V63() V64() V65() V69() set
NAT is non empty V12() epsilon-transitive epsilon-connected ordinal V36() cardinal limit_cardinal V63() V64() V65() V66() V67() V68() V69() Element of K19(REAL)
K19(REAL) is non empty V12() V36() set
ExtREAL is non empty V64() set
K20(NAT,ExtREAL) is Relation-like non empty V12() V36() V54() set
K19(K20(NAT,ExtREAL)) is non empty V12() V36() set
K19(ExtREAL) is non empty set
omega is non empty V12() epsilon-transitive epsilon-connected ordinal V36() cardinal limit_cardinal V63() V64() V65() V66() V67() V68() V69() set
K19(omega) is non empty V12() V36() set
K19(NAT) is non empty V12() V36() set
K204(NAT) is V50() set
COMPLEX is non empty V12() V36() V63() V69() set
RAT is non empty V12() V36() V63() V64() V65() V66() V69() set
INT is non empty V12() V36() V63() V64() V65() V66() V67() V69() set
K20(REAL,REAL) is Relation-like non empty V12() V36() V53() V54() V55() set
K19(K20(REAL,REAL)) is non empty V12() V36() set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
{{},1} is non empty V36() V40() V63() V64() V65() V66() V67() V68() set
K20(COMPLEX,COMPLEX) is Relation-like non empty V12() V36() V53() set
K19(K20(COMPLEX,COMPLEX)) is non empty V12() V36() set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like non empty V12() V36() V53() set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is non empty V12() V36() set
K20(K20(REAL,REAL),REAL) is Relation-like non empty V12() V36() V53() V54() V55() set
K19(K20(K20(REAL,REAL),REAL)) is non empty V12() V36() set
K20(RAT,RAT) is Relation-like RAT -valued non empty V12() V36() V53() V54() V55() set
K19(K20(RAT,RAT)) is non empty V12() V36() set
K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued non empty V12() V36() V53() V54() V55() set
K19(K20(K20(RAT,RAT),RAT)) is non empty V12() V36() set
K20(INT,INT) is Relation-like RAT -valued INT -valued non empty V12() V36() V53() V54() V55() set
K19(K20(INT,INT)) is non empty V12() V36() set
K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued non empty V12() V36() V53() V54() V55() set
K19(K20(K20(INT,INT),INT)) is non empty V12() V36() set
K20(NAT,NAT) is Relation-like RAT -valued INT -valued non empty V12() V36() V53() V54() V55() V56() set
K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued non empty V12() V36() V53() V54() V55() V56() set
K19(K20(K20(NAT,NAT),NAT)) is non empty V12() V36() set
K526() is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg 1 is non empty V12() V36() 1 -element V63() V64() V65() V66() V67() V68() Element of K19(NAT)
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() Element of NAT
-infty is non empty non real ext-real non positive negative set
+infty is non empty non real ext-real positive non negative set
F is ext-real Element of ExtREAL
G is ext-real Element of ExtREAL
F * G is ext-real set
F is ext-real Element of ExtREAL
s is complex real ext-real Element of REAL
G is ext-real Element of ExtREAL
F is complex real ext-real Element of REAL
(F,G) is ext-real Element of ExtREAL
s * F is complex real ext-real Element of REAL
F is ext-real Element of ExtREAL
G is ext-real Element of ExtREAL
F / G is ext-real set
G " is ext-real set
F * (G ") is ext-real set
F is ext-real Element of ExtREAL
G is ext-real Element of ExtREAL
(F,G) is ext-real Element of ExtREAL
G " is ext-real set
F * (G ") is ext-real set
s is complex real ext-real Element of REAL
F is complex real ext-real Element of REAL
s / F is complex real ext-real Element of REAL
F " is complex real ext-real set
s * (F ") is complex real ext-real set
s1 is complex set
s1 " is complex Element of COMPLEX
G is complex real ext-real set
G * (s1 ") is complex Element of COMPLEX
s is complex real ext-real set
G / s is complex real ext-real Element of REAL
s " is complex real ext-real set
G * (s ") is complex real ext-real set
F is ext-real Element of ExtREAL
- F is ext-real Element of ExtREAL
s is ext-real Element of ExtREAL
G is ext-real Element of ExtREAL
- s is ext-real Element of ExtREAL
- G is ext-real Element of ExtREAL
F is ext-real Element of ExtREAL
(F) is ext-real Element of ExtREAL
F is ext-real Element of ExtREAL
(F) is ext-real Element of ExtREAL
- F is ext-real Element of ExtREAL
F is ext-real Element of ExtREAL
(F) is ext-real Element of ExtREAL
- F is ext-real Element of ExtREAL
F is complex real ext-real Element of REAL
G is complex real ext-real Element of REAL
F * G is complex real ext-real Element of REAL
R_EAL F is ext-real Element of ExtREAL
R_EAL G is ext-real Element of ExtREAL
((R_EAL F),(R_EAL G)) is ext-real Element of ExtREAL
F is complex real ext-real Element of REAL
G is complex real ext-real Element of REAL
F / G is complex real ext-real Element of REAL
G " is complex real ext-real set
F * (G ") is complex real ext-real set
R_EAL F is ext-real Element of ExtREAL
R_EAL G is ext-real Element of ExtREAL
((R_EAL F),(R_EAL G)) is ext-real Element of ExtREAL
(R_EAL G) " is ext-real set
(R_EAL F) * ((R_EAL G) ") is ext-real set
F is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
0. is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() Element of ExtREAL
G is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s is ext-real Element of ExtREAL
<*s*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V36() 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
G ^ <*s*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len (G ^ <*s*>) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F is Relation-like NAT -defined ExtREAL -valued Function-like non empty total quasi_total V54() Element of K19(K20(NAT,ExtREAL))
F . 0 is ext-real Element of ExtREAL
F is Relation-like NAT -defined ExtREAL -valued Function-like non empty total quasi_total V54() Element of K19(K20(NAT,ExtREAL))
F . 0 is ext-real Element of ExtREAL
(len G) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F . (len G) is ext-real Element of ExtREAL
(F . (len G)) + s is ext-real Element of ExtREAL
G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F . G is ext-real Element of ExtREAL
G is Relation-like NAT -defined ExtREAL -valued Function-like non empty total quasi_total V54() Element of K19(K20(NAT,ExtREAL))
G . 0 is ext-real Element of ExtREAL
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
G . (s + 1) is ext-real Element of ExtREAL
G . s is ext-real Element of ExtREAL
(G ^ <*s*>) . (s + 1) is ext-real Element of ExtREAL
(G . s) + ((G ^ <*s*>) . (s + 1)) is ext-real Element of ExtREAL
len <*s*> is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(len G) + (len <*s*>) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F . s is ext-real Element of ExtREAL
Seg (len G) is V36() len G -element V63() V64() V65() V66() V67() V68() Element of K19(NAT)
dom G is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
F . (s + 1) is ext-real Element of ExtREAL
G . (s + 1) is ext-real Element of ExtREAL
(G . s) + (G . (s + 1)) is ext-real Element of ExtREAL
(G . s) + s is ext-real Element of ExtREAL
<*> ExtREAL is Relation-like non-empty empty-yielding NAT -defined ExtREAL -valued RAT -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() FinSequence of ExtREAL
len (<*> ExtREAL) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() Element of NAT
NAT --> 0. is Relation-like NAT -defined ExtREAL -valued INT -valued Function-like non empty total quasi_total T-Sequence-like V53() V54() V55() V56() Element of K19(K20(NAT,ExtREAL))
G is Relation-like NAT -defined ExtREAL -valued Function-like non empty total quasi_total V54() Element of K19(K20(NAT,ExtREAL))
G . 0 is ext-real Element of ExtREAL
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
G . (s + 1) is ext-real Element of ExtREAL
G . s is ext-real Element of ExtREAL
(<*> ExtREAL) . (s + 1) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() Element of ExtREAL
(G . s) + ((<*> ExtREAL) . (s + 1)) is ext-real Element of ExtREAL
G is Relation-like NAT -defined ExtREAL -valued Function-like non empty total quasi_total V54() Element of K19(K20(NAT,ExtREAL))
G . 0 is ext-real Element of ExtREAL
G . (len F) is ext-real Element of ExtREAL
G is ext-real Element of ExtREAL
s is ext-real Element of ExtREAL
F is Relation-like NAT -defined ExtREAL -valued Function-like non empty total quasi_total V54() Element of K19(K20(NAT,ExtREAL))
F . (len F) is ext-real Element of ExtREAL
F . 0 is ext-real Element of ExtREAL
G is Relation-like NAT -defined ExtREAL -valued Function-like non empty total quasi_total V54() Element of K19(K20(NAT,ExtREAL))
G . (len F) is ext-real Element of ExtREAL
G . 0 is ext-real Element of ExtREAL
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F . s is ext-real Element of ExtREAL
G . s is ext-real Element of ExtREAL
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F . (s + 1) is ext-real Element of ExtREAL
G . (s + 1) is ext-real Element of ExtREAL
F . (s + 1) is ext-real Element of ExtREAL
(F . s) + (F . (s + 1)) is ext-real Element of ExtREAL
<*> ExtREAL is Relation-like non-empty empty-yielding NAT -defined ExtREAL -valued RAT -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() FinSequence of ExtREAL
((<*> ExtREAL)) is ext-real Element of ExtREAL
F is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
(F) is ext-real Element of ExtREAL
len F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
G is Relation-like NAT -defined ExtREAL -valued Function-like non empty total quasi_total V54() Element of K19(K20(NAT,ExtREAL))
G . (len F) is ext-real Element of ExtREAL
G . 0 is ext-real Element of ExtREAL
F is ext-real Element of ExtREAL
<*F*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V36() 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
(<*F*>) is ext-real Element of ExtREAL
len <*F*> is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s is Relation-like NAT -defined ExtREAL -valued Function-like non empty total quasi_total V54() Element of K19(K20(NAT,ExtREAL))
s . (len <*F*>) is ext-real Element of ExtREAL
s . 0 is ext-real Element of ExtREAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s . (0 + 1) is ext-real Element of ExtREAL
<*F*> . (0 + 1) is ext-real Element of ExtREAL
(s . 0) + (<*F*> . (0 + 1)) is ext-real Element of ExtREAL
s . 1 is ext-real Element of ExtREAL
<*F*> . 1 is ext-real Element of ExtREAL
F is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
(F) is ext-real Element of ExtREAL
G is ext-real Element of ExtREAL
<*G*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V36() 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
F ^ <*G*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
((F ^ <*G*>)) is ext-real Element of ExtREAL
(F) + G is ext-real Element of ExtREAL
len (F ^ <*G*>) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s is Relation-like NAT -defined ExtREAL -valued Function-like non empty total quasi_total V54() Element of K19(K20(NAT,ExtREAL))
s . (len (F ^ <*G*>)) is ext-real Element of ExtREAL
s . 0 is ext-real Element of ExtREAL
len F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
len <*G*> is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(len F) + (len <*G*>) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(len F) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s . (F + 1) is ext-real Element of ExtREAL
s . F is ext-real Element of ExtREAL
F . (F + 1) is ext-real Element of ExtREAL
(s . F) + (F . (F + 1)) is ext-real Element of ExtREAL
Seg (len F) is V36() len F -element V63() V64() V65() V66() V67() V68() Element of K19(NAT)
dom F is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
(F ^ <*G*>) . (F + 1) is ext-real Element of ExtREAL
(s . F) + ((F ^ <*G*>) . (F + 1)) is ext-real Element of ExtREAL
s . (len F) is ext-real Element of ExtREAL
s . ((len F) + 1) is ext-real Element of ExtREAL
(F ^ <*G*>) . ((len F) + 1) is ext-real Element of ExtREAL
(s . (len F)) + ((F ^ <*G*>) . ((len F) + 1)) is ext-real Element of ExtREAL
F is ext-real Element of ExtREAL
G is ext-real Element of ExtREAL
<*F,G*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V36() 2 -element FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
(<*F,G*>) is ext-real Element of ExtREAL
F + G is ext-real Element of ExtREAL
<*F*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V36() 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
<*G*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V36() 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
<*F*> ^ <*G*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V36() 1 + 1 -element FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
((<*F*> ^ <*G*>)) is ext-real Element of ExtREAL
(<*F*>) is ext-real Element of ExtREAL
(<*F*>) + G is ext-real Element of ExtREAL
-infty is non empty non real ext-real non positive negative Element of ExtREAL
F is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng F is V36() V64() Element of K19(ExtREAL)
(F) is ext-real Element of ExtREAL
G is ext-real Element of ExtREAL
<*G*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V36() 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
F ^ <*G*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng (F ^ <*G*>) is non empty V36() V64() Element of K19(ExtREAL)
((F ^ <*G*>)) is ext-real Element of ExtREAL
(F) + G is ext-real Element of ExtREAL
rng <*G*> is non empty V12() V36() 1 -element V64() Element of K19(ExtREAL)
(rng F) \/ (rng <*G*>) is non empty V36() V64() Element of K19(ExtREAL)
{G} is non empty V12() V36() 1 -element V64() Element of K19(ExtREAL)
rng (<*> ExtREAL) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V53() V54() V55() V56() V57() V58() V59() V60() V63() V64() V65() V66() V67() V68() V69() V94() Element of K19(ExtREAL)
F is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng F is V36() V64() Element of K19(ExtREAL)
G is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng G is V36() V64() Element of K19(ExtREAL)
F ^ G is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
((F ^ G)) is ext-real Element of ExtREAL
(F) is ext-real Element of ExtREAL
(G) is ext-real Element of ExtREAL
(F) + (G) is ext-real Element of ExtREAL
s is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng s is V36() V64() Element of K19(ExtREAL)
F ^ s is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
((F ^ s)) is ext-real Element of ExtREAL
(s) is ext-real Element of ExtREAL
(F) + (s) is ext-real Element of ExtREAL
F is ext-real Element of ExtREAL
<*F*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V36() 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
s ^ <*F*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng (s ^ <*F*>) is non empty V36() V64() Element of K19(ExtREAL)
F ^ (s ^ <*F*>) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
((F ^ (s ^ <*F*>))) is ext-real Element of ExtREAL
((s ^ <*F*>)) is ext-real Element of ExtREAL
(F) + ((s ^ <*F*>)) is ext-real Element of ExtREAL
rng <*F*> is non empty V12() V36() 1 -element V64() Element of K19(ExtREAL)
(rng s) \/ (rng <*F*>) is non empty V36() V64() Element of K19(ExtREAL)
{F} is non empty V12() V36() 1 -element V64() Element of K19(ExtREAL)
(F ^ s) ^ <*F*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
((F) + (s)) + F is ext-real Element of ExtREAL
(s) + F is ext-real Element of ExtREAL
(F) + ((s) + F) is ext-real Element of ExtREAL
rng (<*> ExtREAL) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V53() V54() V55() V56() V57() V58() V59() V60() V63() V64() V65() V66() V67() V68() V69() V94() Element of K19(ExtREAL)
F ^ (<*> ExtREAL) is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
((F ^ (<*> ExtREAL))) is ext-real Element of ExtREAL
(F) + ((<*> ExtREAL)) is ext-real Element of ExtREAL
rng (<*> ExtREAL) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V53() V54() V55() V56() V57() V58() V59() V60() V63() V64() V65() V66() V67() V68() V69() V94() Element of K19(REAL)
G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() set
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() set
F + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg (F + 1) is non empty V36() F + 1 -element V63() V64() V65() V66() V67() V68() Element of K19(NAT)
K20((Seg (F + 1)),(Seg (F + 1))) is Relation-like RAT -valued INT -valued non empty V36() V53() V54() V55() V56() set
K19(K20((Seg (F + 1)),(Seg (F + 1)))) is non empty V36() V40() set
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s - 1 is complex real ext-real V51() V52() Element of INT
- 1 is complex real ext-real non positive V51() set
s + (- 1) is complex real ext-real V51() set
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of NAT
dom s is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s /. F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F - 1 is complex real ext-real V51() V52() Element of INT
- 1 is complex real ext-real non positive V51() set
F + (- 1) is complex real ext-real V51() set
(F + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s . F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
F - 1 is complex real ext-real V51() V52() Element of INT
- 1 is complex real ext-real non positive V51() set
F + (- 1) is complex real ext-real V51() set
s /. F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
rng s is V36() V63() V64() V65() V66() V67() V68() Element of K19(REAL)
F is set
G is set
s . G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s - 1 is complex real ext-real V51() V52() Element of INT
- 1 is complex real ext-real non positive V51() set
s + (- 1) is complex real ext-real V51() set
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s . G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s . (G + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
(G + 1) - 1 is complex real ext-real V51() V52() Element of INT
- 1 is complex real ext-real non positive V51() set
(G + 1) + (- 1) is complex real ext-real V51() set
s . G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s /. F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F - 1 is complex real ext-real V51() V52() Element of INT
- 1 is complex real ext-real non positive V51() set
F + (- 1) is complex real ext-real V51() set
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(F - 1) + 1 is complex real ext-real V51() V52() Element of INT
F is set
G is set
s . F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
s . G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s /. s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s . s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s /. s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s . s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
s - 1 is complex real ext-real V51() V52() Element of INT
- 1 is complex real ext-real non positive V51() set
s + (- 1) is complex real ext-real V51() set
s1 - 1 is complex real ext-real V51() V52() Element of INT
s1 + (- 1) is complex real ext-real V51() set
F is Relation-like Seg (F + 1) -defined Seg (F + 1) -valued Function-like one-to-one non empty total quasi_total onto bijective V36() V53() V54() V55() V56() Element of K19(K20((Seg (F + 1)),(Seg (F + 1))))
G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F . G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
G - 1 is complex real ext-real V51() V52() Element of INT
- 1 is complex real ext-real non positive V51() set
G + (- 1) is complex real ext-real V51() set
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() set
F + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg (F + 1) is non empty V36() F + 1 -element V63() V64() V65() V66() V67() V68() Element of K19(NAT)
K20((Seg (F + 1)),(Seg (F + 1))) is Relation-like RAT -valued INT -valued non empty V36() V53() V54() V55() V56() set
K19(K20((Seg (F + 1)),(Seg (F + 1)))) is non empty V36() V40() set
G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() set
Seg F is V36() F -element V63() V64() V65() V66() V67() V68() Element of K19(NAT)
K20((Seg F),(Seg F)) is Relation-like RAT -valued INT -valued V36() V53() V54() V55() V56() set
K19(K20((Seg F),(Seg F))) is non empty V36() V40() set
s is Relation-like Seg (F + 1) -defined Seg (F + 1) -valued Function-like one-to-one non empty total quasi_total onto bijective V36() V53() V54() V55() V56() Element of K19(K20((Seg (F + 1)),(Seg (F + 1))))
s . (F + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
F is Relation-like Seg (F + 1) -defined Seg (F + 1) -valued Function-like one-to-one non empty total quasi_total onto bijective V36() V53() V54() V55() V56() Element of K19(K20((Seg (F + 1)),(Seg (F + 1))))
G is Relation-like NAT -defined Seg (F + 1) -valued Function-like V36() FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of Seg (F + 1)
G | F is Relation-like NAT -defined Seg (F + 1) -valued Function-like V36() FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of Seg (F + 1)
F * (G | F) is Relation-like NAT -defined RAT -valued Seg (F + 1) -valued Function-like V36() V53() V54() V55() V56() Element of K19(K20(NAT,(Seg (F + 1))))
K20(NAT,(Seg (F + 1))) is Relation-like RAT -valued INT -valued non empty V12() V36() V53() V54() V55() V56() set
K19(K20(NAT,(Seg (F + 1)))) is non empty V12() V36() set
dom F is non empty V36() V63() V64() V65() V66() V67() V68() Element of K19((Seg (F + 1)))
K19((Seg (F + 1))) is non empty V36() V40() set
0 + F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
1 + F is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
G | (Seg F) is Relation-like NAT -defined Seg F -defined NAT -defined RAT -valued Seg (F + 1) -valued Function-like V36() FinSubsequence-like V53() V54() V55() V56() Element of K19(K20(NAT,(Seg (F + 1))))
rng F is non empty V36() V63() V64() V65() V66() V67() V68() Element of K19(REAL)
dom s is non empty V36() V63() V64() V65() V66() V67() V68() Element of K19((Seg (F + 1)))
len G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
len (G | F) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s is Relation-like NAT -defined Seg (F + 1) -valued Function-like V36() FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of Seg (F + 1)
len s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom s is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
rng s is non empty V36() V63() V64() V65() V66() V67() V68() Element of K19(REAL)
rng s is V36() V63() V64() V65() V66() V67() V68() Element of K19(REAL)
s1 is set
s9 is set
s . s9 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
q is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(G | F) . q is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
s . q is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
F . (s . q) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
p2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p2 - 1 is complex real ext-real V51() V52() Element of INT
- 1 is complex real ext-real non positive V51() set
p2 + (- 1) is complex real ext-real V51() set
s9 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F . s9 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
q is set
s . q is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(G | F) . p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
s . p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
s . p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
s9 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
q is set
s . q is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F . (s9 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
(s9 + 1) - 1 is complex real ext-real V51() V52() Element of INT
- 1 is complex real ext-real non positive V51() set
(s9 + 1) + (- 1) is complex real ext-real V51() set
(G | F) . p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
s . p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
s . p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
F . (s . p) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
s9 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() set
F + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg (F + 1) is non empty V36() F + 1 -element V63() V64() V65() V66() V67() V68() Element of K19(NAT)
K20((Seg (F + 1)),(Seg (F + 1))) is Relation-like RAT -valued INT -valued non empty V36() V53() V54() V55() V56() set
K19(K20((Seg (F + 1)),(Seg (F + 1)))) is non empty V36() V40() set
G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() set
s is Relation-like Seg (F + 1) -defined Seg (F + 1) -valued Function-like one-to-one non empty total quasi_total onto bijective V36() V53() V54() V55() V56() Element of K19(K20((Seg (F + 1)),(Seg (F + 1))))
F is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
G is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
G * s is Relation-like Seg (F + 1) -defined ExtREAL -valued Function-like V36() V54() Element of K19(K20((Seg (F + 1)),ExtREAL))
K20((Seg (F + 1)),ExtREAL) is Relation-like non empty V54() set
K19(K20((Seg (F + 1)),ExtREAL)) is non empty set
len G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
rng G is V36() V64() Element of K19(ExtREAL)
(F) is ext-real Element of ExtREAL
(G) is ext-real Element of ExtREAL
1 - 1 is complex real ext-real V51() V52() Element of INT
- 1 is complex real ext-real non positive V51() set
1 + (- 1) is complex real ext-real V51() set
G - 1 is complex real ext-real V51() V52() Element of INT
G + (- 1) is complex real ext-real V51() set
G -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
G | F is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
(G | F) | (G -' 1) is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
(G | F) /^ (G -' 1) is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
((G | F) | (G -' 1)) ^ ((G | F) /^ (G -' 1)) is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
dom s is non empty V36() V63() V64() V65() V66() V67() V68() Element of K19((Seg (F + 1)))
K19((Seg (F + 1))) is non empty V36() V40() set
s1 is Relation-like NAT -defined Seg (F + 1) -valued Function-like V36() FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of Seg (F + 1)
len s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(F + 1) - 1 is complex real ext-real V51() V52() Element of INT
(F + 1) + (- 1) is complex real ext-real V51() set
dom G is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
len F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F /^ G is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len (F /^ G) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(F + 1) - G is complex real ext-real V51() V52() Element of INT
- G is complex real ext-real non positive V51() set
(F + 1) + (- G) is complex real ext-real V51() set
F | (G -' 1) is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len (F | (G -' 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom F is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
s9 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() set
(F | (G -' 1)) . s9 is ext-real Element of ExtREAL
((G | F) | (G -' 1)) . s9 is ext-real Element of ExtREAL
F . s9 is ext-real Element of ExtREAL
(G | F) . s9 is ext-real Element of ExtREAL
G . s9 is ext-real Element of ExtREAL
(G -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s . s9 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
G . (s . s9) is ext-real Element of ExtREAL
0 + F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
1 + F is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
len (G | F) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
len ((G | F) | (G -' 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
len ((G | F) /^ (G -' 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F - (G - 1) is complex real ext-real V51() V52() Element of INT
- (G - 1) is complex real ext-real V51() set
F + (- (G - 1)) is complex real ext-real V51() set
q is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() set
(F /^ G) . q is ext-real Element of ExtREAL
((G | F) /^ (G -' 1)) . q is ext-real Element of ExtREAL
q + G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s9 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg s9 is V36() s9 -element V63() V64() V65() V66() V67() V68() Element of K19(NAT)
dom ((G | F) /^ (G -' 1)) is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
q + (G -' 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(G | F) . (q + (G -' 1)) is ext-real Element of ExtREAL
(q + G) - 1 is complex real ext-real V51() V52() Element of INT
(q + G) + (- 1) is complex real ext-real V51() set
G . ((q + G) - 1) is ext-real Element of ExtREAL
F . (q + G) is ext-real Element of ExtREAL
s . (q + G) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
G . (s . (q + G)) is ext-real Element of ExtREAL
dom (F /^ G) is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
1 + G is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F . G is ext-real Element of ExtREAL
<*(F . G)*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V36() 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
(F | (G -' 1)) ^ <*(F . G)*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
((F | (G -' 1)) ^ <*(F . G)*>) ^ (F /^ G) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng F is V36() V64() Element of K19(ExtREAL)
rng ((F | (G -' 1)) ^ <*(F . G)*>) is non empty V36() V64() Element of K19(ExtREAL)
rng (F /^ G) is V36() V64() Element of K19(ExtREAL)
(rng ((F | (G -' 1)) ^ <*(F . G)*>)) \/ (rng (F /^ G)) is non empty V36() V64() Element of K19(ExtREAL)
s . G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
G . (F + 1) is ext-real Element of ExtREAL
Seg F is V36() F -element V63() V64() V65() V66() V67() V68() Element of K19(NAT)
G | (Seg F) is Relation-like NAT -defined Seg F -defined NAT -defined ExtREAL -valued Function-like V36() FinSubsequence-like V54() Element of K19(K20(NAT,ExtREAL))
rng (G | F) is V36() V64() Element of K19(ExtREAL)
rng ((G | F) | (G -' 1)) is V36() V64() Element of K19(ExtREAL)
rng ((G | F) /^ (G -' 1)) is V36() V64() Element of K19(ExtREAL)
(rng ((G | F) | (G -' 1))) \/ (rng ((G | F) /^ (G -' 1))) is V36() V64() Element of K19(ExtREAL)
rng (F | (G -' 1)) is V36() V64() Element of K19(ExtREAL)
rng <*(F . G)*> is non empty V12() V36() 1 -element V64() Element of K19(ExtREAL)
(rng (F | (G -' 1))) \/ (rng <*(F . G)*>) is non empty V36() V64() Element of K19(ExtREAL)
((F | (G -' 1))) is ext-real Element of ExtREAL
{(F . G)} is non empty V12() V36() 1 -element V64() Element of K19(ExtREAL)
((F /^ G)) is ext-real Element of ExtREAL
G | (F + 1) is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
G | (Seg (F + 1)) is Relation-like NAT -defined Seg (F + 1) -defined NAT -defined ExtREAL -valued Function-like V36() FinSubsequence-like V54() Element of K19(K20(NAT,ExtREAL))
<*(G . (F + 1))*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V36() 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
(G | F) ^ <*(G . (F + 1))*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
(((F | (G -' 1)) ^ <*(F . G)*>)) is ext-real Element of ExtREAL
(((F | (G -' 1)) ^ <*(F . G)*>)) + ((F /^ G)) is ext-real Element of ExtREAL
((F | (G -' 1))) + (F . G) is ext-real Element of ExtREAL
(((F | (G -' 1))) + (F . G)) + ((F /^ G)) is ext-real Element of ExtREAL
((F | (G -' 1))) + ((F /^ G)) is ext-real Element of ExtREAL
(((F | (G -' 1))) + ((F /^ G))) + (F . G) is ext-real Element of ExtREAL
(((G | F) | (G -' 1))) is ext-real Element of ExtREAL
(((G | F) /^ (G -' 1))) is ext-real Element of ExtREAL
(((G | F) | (G -' 1))) + (((G | F) /^ (G -' 1))) is ext-real Element of ExtREAL
((((G | F) | (G -' 1))) + (((G | F) /^ (G -' 1)))) + (G . (F + 1)) is ext-real Element of ExtREAL
((G | F)) is ext-real Element of ExtREAL
((G | F)) + (G . (F + 1)) is ext-real Element of ExtREAL
F is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
dom F is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
K20((dom F),(dom F)) is Relation-like RAT -valued INT -valued V36() V53() V54() V55() V56() set
K19(K20((dom F),(dom F))) is non empty V36() V40() set
G is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng F is V36() V64() Element of K19(ExtREAL)
(F) is ext-real Element of ExtREAL
(G) is ext-real Element of ExtREAL
s is Relation-like dom F -defined dom F -valued Function-like one-to-one total quasi_total onto bijective V36() V53() V54() V55() V56() Element of K19(K20((dom F),(dom F)))
F * s is Relation-like dom F -defined ExtREAL -valued Function-like V36() V54() Element of K19(K20((dom F),ExtREAL))
K20((dom F),ExtREAL) is Relation-like V54() set
K19(K20((dom F),ExtREAL)) is non empty set
Seg 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V36() V37() V40() cardinal 0 -element {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() Element of K19(NAT)
K20((Seg 0),(Seg 0)) is Relation-like RAT -valued INT -valued V36() V53() V54() V55() V56() set
K19(K20((Seg 0),(Seg 0))) is non empty V36() V40() set
F is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
G is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng F is V36() V64() Element of K19(ExtREAL)
(F) is ext-real Element of ExtREAL
(G) is ext-real Element of ExtREAL
s is Relation-like non-empty empty-yielding Seg 0 -defined Seg 0 -valued Function-like one-to-one constant functional empty total quasi_total onto bijective epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() Element of K19(K20((Seg 0),(Seg 0)))
F * s is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined ExtREAL -valued RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() Element of K19(K20((Seg 0),ExtREAL))
K20((Seg 0),ExtREAL) is Relation-like V54() set
K19(K20((Seg 0),ExtREAL)) is non empty set
F is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() set
Seg F is non empty V36() F -element V63() V64() V65() V66() V67() V68() Element of K19(NAT)
K20((Seg F),(Seg F)) is Relation-like RAT -valued INT -valued non empty V36() V53() V54() V55() V56() set
K19(K20((Seg F),(Seg F))) is non empty V36() V40() set
F + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg (F + 1) is non empty V36() F + 1 -element V63() V64() V65() V66() V67() V68() Element of K19(NAT)
K20((Seg (F + 1)),(Seg (F + 1))) is Relation-like RAT -valued INT -valued non empty V36() V53() V54() V55() V56() set
K19(K20((Seg (F + 1)),(Seg (F + 1)))) is non empty V36() V40() set
G is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng G is V36() V64() Element of K19(ExtREAL)
(G) is ext-real Element of ExtREAL
(s) is ext-real Element of ExtREAL
s1 is Relation-like Seg (F + 1) -defined Seg (F + 1) -valued Function-like one-to-one non empty total quasi_total onto bijective V36() V53() V54() V55() V56() Element of K19(K20((Seg (F + 1)),(Seg (F + 1))))
G * s1 is Relation-like Seg (F + 1) -defined ExtREAL -valued Function-like V36() V54() Element of K19(K20((Seg (F + 1)),ExtREAL))
K20((Seg (F + 1)),ExtREAL) is Relation-like non empty V54() set
K19(K20((Seg (F + 1)),ExtREAL)) is non empty set
rng s1 is non empty V36() V63() V64() V65() V66() V67() V68() Element of K19(REAL)
dom s1 is non empty V36() V63() V64() V65() V66() V67() V68() Element of K19((Seg (F + 1)))
K19((Seg (F + 1))) is non empty V36() V40() set
s1 . (F + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
q is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p is Relation-like Seg (F + 1) -defined Seg (F + 1) -valued Function-like one-to-one non empty total quasi_total onto bijective V36() V53() V54() V55() V56() Element of K19(K20((Seg (F + 1)),(Seg (F + 1))))
p " is Relation-like Seg (F + 1) -defined Seg (F + 1) -valued Function-like one-to-one non empty total quasi_total onto bijective V36() V53() V54() V55() V56() Element of K19(K20((Seg (F + 1)),(Seg (F + 1))))
dom p is non empty V36() V63() V64() V65() V66() V67() V68() Element of K19((Seg (F + 1)))
p . q is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
G . (s1 . (F + 1)) is ext-real Element of ExtREAL
p2 is Relation-like NAT -defined Seg (F + 1) -valued Function-like V36() FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of Seg (F + 1)
p2 . (F + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
G . (p2 . (F + 1)) is ext-real Element of ExtREAL
0 + F is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
1 + F is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom G is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
G * p2 is Relation-like NAT -defined ExtREAL -valued Function-like V36() V54() Element of K19(K20(NAT,ExtREAL))
H is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
H * p is Relation-like Seg (F + 1) -defined ExtREAL -valued Function-like V36() V54() Element of K19(K20((Seg (F + 1)),ExtREAL))
p2 * p is Relation-like Seg (F + 1) -defined RAT -valued Seg (F + 1) -valued Function-like V36() V53() V54() V55() V56() Element of K19(K20((Seg (F + 1)),(Seg (F + 1))))
G * (p2 * p) is Relation-like Seg (F + 1) -defined ExtREAL -valued Function-like V36() V54() Element of K19(K20((Seg (F + 1)),ExtREAL))
id (Seg (F + 1)) is Relation-like Seg (F + 1) -defined Seg (F + 1) -valued RAT -valued INT -valued Function-like one-to-one non empty total quasi_total V36() V53() V54() V55() V56() V57() V59() Element of K19(K20((Seg (F + 1)),(Seg (F + 1))))
G * (id (Seg (F + 1))) is Relation-like Seg (F + 1) -defined ExtREAL -valued Function-like V36() V54() Element of K19(K20((Seg (F + 1)),ExtREAL))
s9 is Relation-like NAT -defined Seg (F + 1) -valued Function-like V36() FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of Seg (F + 1)
len s9 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
len s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom s is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
s . (F + 1) is ext-real Element of ExtREAL
s9 | F is Relation-like NAT -defined Seg (F + 1) -valued Function-like V36() FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of Seg (F + 1)
p * (s9 | F) is Relation-like NAT -defined RAT -valued Seg (F + 1) -valued Function-like V36() V53() V54() V55() V56() Element of K19(K20(NAT,(Seg (F + 1))))
K20(NAT,(Seg (F + 1))) is Relation-like RAT -valued INT -valued non empty V12() V36() V53() V54() V55() V56() set
K19(K20(NAT,(Seg (F + 1)))) is non empty V12() V36() set
p1 is Relation-like Seg F -defined Seg F -valued Function-like one-to-one non empty total quasi_total onto bijective V36() V53() V54() V55() V56() Element of K19(K20((Seg F),(Seg F)))
dom p1 is non empty V36() V63() V64() V65() V66() V67() V68() Element of K19((Seg F))
K19((Seg F)) is non empty V36() V40() set
rng H is V36() V64() Element of K19(ExtREAL)
dom p2 is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
rng p is non empty V36() V63() V64() V65() V66() V67() V68() Element of K19(REAL)
len p2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
len H is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom H is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
H | F is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len (H | F) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s | F is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
(H | F) * p1 is Relation-like Seg F -defined ExtREAL -valued Function-like V36() V54() Element of K19(K20((Seg F),ExtREAL))
K20((Seg F),ExtREAL) is Relation-like non empty V54() set
K19(K20((Seg F),ExtREAL)) is non empty set
dom (H | F) is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
p19 is Relation-like NAT -defined Seg F -valued Function-like V36() FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of Seg F
(H | F) * p19 is Relation-like NAT -defined ExtREAL -valued Function-like V36() V54() Element of K19(K20(NAT,ExtREAL))
len p19 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
H1 is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len H1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() set
(s | F) . i is ext-real Element of ExtREAL
((H | F) * p1) . i is ext-real Element of ExtREAL
s1 . i is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
dom H1 is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
p1 . i is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
(H | F) . (p1 . i) is ext-real Element of ExtREAL
rng p1 is non empty V36() V63() V64() V65() V66() V67() V68() Element of K19(REAL)
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
H . (p1 . i) is ext-real Element of ExtREAL
(s9 | F) . i is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
p . (s1 . i) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
s . i is ext-real Element of ExtREAL
p2 . (p1 . i) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() Element of ExtREAL
G . (p2 . (p1 . i)) is ext-real Element of ExtREAL
G . (s1 . i) is ext-real Element of ExtREAL
len (s | F) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s | (Seg F) is Relation-like NAT -defined Seg F -defined NAT -defined ExtREAL -valued Function-like V36() FinSubsequence-like V54() Element of K19(K20(NAT,ExtREAL))
<*(s . (F + 1))*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V36() 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
(s | F) ^ <*(s . (F + 1))*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
((s | F)) is ext-real Element of ExtREAL
((s | F)) + (s . (F + 1)) is ext-real Element of ExtREAL
H | (Seg F) is Relation-like NAT -defined Seg F -defined NAT -defined ExtREAL -valued Function-like V36() FinSubsequence-like V54() Element of K19(K20(NAT,ExtREAL))
H . (F + 1) is ext-real Element of ExtREAL
<*(H . (F + 1))*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V36() 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
(H | F) ^ <*(H . (F + 1))*> is Relation-like NAT -defined ExtREAL -valued Function-like non empty V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
(H) is ext-real Element of ExtREAL
((H | F)) is ext-real Element of ExtREAL
((H | F)) + (H . (F + 1)) is ext-real Element of ExtREAL
rng (H | F) is V36() V64() Element of K19(ExtREAL)
K20((Seg 1),(Seg 1)) is Relation-like RAT -valued INT -valued non empty V36() V53() V54() V55() V56() set
K19(K20((Seg 1),(Seg 1))) is non empty V36() V40() set
F is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
G is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng F is V36() V64() Element of K19(ExtREAL)
(F) is ext-real Element of ExtREAL
(G) is ext-real Element of ExtREAL
s is Relation-like Seg 1 -defined Seg 1 -valued Function-like one-to-one non empty total quasi_total onto bijective V36() V53() V54() V55() V56() Element of K19(K20((Seg 1),(Seg 1)))
F * s is Relation-like Seg 1 -defined ExtREAL -valued Function-like V36() V54() Element of K19(K20((Seg 1),ExtREAL))
K20((Seg 1),ExtREAL) is Relation-like non empty V54() set
K19(K20((Seg 1),ExtREAL)) is non empty set
dom s is non empty V12() V36() 1 -element V63() V64() V65() V66() V67() V68() Element of K19((Seg 1))
K19((Seg 1)) is non empty V36() V40() set
s1 is Relation-like NAT -defined Seg 1 -valued Function-like V36() FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of Seg 1
len s1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom F is V36() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
len G is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
G . 1 is ext-real Element of ExtREAL
<*(G . 1)*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V36() 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
rng G is V36() V64() Element of K19(ExtREAL)
{(G . 1)} is non empty V12() V36() 1 -element V64() Element of K19(ExtREAL)
F . 1 is ext-real Element of ExtREAL
<*(F . 1)*> is Relation-like NAT -defined ExtREAL -valued Function-like constant non empty V12() V36() 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
{(F . 1)} is non empty V12() V36() 1 -element V64() Element of K19(ExtREAL)
len F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg (len F) is V36() len F -element V63() V64() V65() V66() V67() V68() Element of K19(NAT)
K20((Seg (len F)),(Seg (len F))) is Relation-like RAT -valued INT -valued V36() V53() V54() V55() V56() set
K19(K20((Seg (len F)),(Seg (len F)))) is non empty V36() V40() set
F is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len F is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V36() cardinal V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
G is Relation-like NAT -defined ExtREAL -valued Function-like V36() FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
s is Relation-like Seg (len F) -defined Seg (len F) -valued Function-like one-to-one total quasi_total onto bijective V36() V53() V54() V55() V56() Element of K19(K20((Seg (len F)),(Seg (len F))))
F * s is Relation-like Seg (len F) -defined ExtREAL -valued Function-like V36() V54() Element of K19(K20((Seg (len F)),ExtREAL))
K20((Seg (len F)),ExtREAL) is Relation-like V54() set
K19(K20((Seg (len F)),ExtREAL)) is non empty set
rng F is V36() V64() Element of K19(ExtREAL)
(F) is ext-real Element of ExtREAL
(G) is ext-real Element of ExtREAL