REAL is non empty V53() V54() V55() V59() V60() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V53() V54() V55() V56() V57() V58() V59() V60() cardinal limit_cardinal Element of bool REAL
bool REAL is V60() set
RAT is non empty V53() V54() V55() V56() V59() V60() set
0 is Relation-like non-zero 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 ext-real non positive non negative real V41() complex-valued ext-real-valued real-valued natural-valued V53() V54() V55() V56() V57() V58() V59() V60() Function-yielding V70() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered set
COMPLEX is non empty V53() V59() V60() set
INT is non empty V53() V54() V55() V56() V57() V59() V60() set
[:COMPLEX,COMPLEX:] is Relation-like complex-valued V60() set
bool [:COMPLEX,COMPLEX:] is V60() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like complex-valued V60() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is V60() set
[:REAL,REAL:] is Relation-like complex-valued ext-real-valued real-valued V60() set
bool [:REAL,REAL:] is V60() set
[:[:REAL,REAL:],REAL:] is Relation-like complex-valued ext-real-valued real-valued V60() set
bool [:[:REAL,REAL:],REAL:] is V60() set
[:RAT,RAT:] is Relation-like RAT -valued complex-valued ext-real-valued real-valued V60() set
bool [:RAT,RAT:] is V60() set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued complex-valued ext-real-valued real-valued V60() set
bool [:[:RAT,RAT:],RAT:] is V60() set
[:INT,INT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued V60() set
bool [:INT,INT:] is V60() set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued V60() set
bool [:[:INT,INT:],INT:] is V60() set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued V60() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued V60() set
bool [:[:NAT,NAT:],NAT:] is V60() set
omega is non empty epsilon-transitive epsilon-connected ordinal V53() V54() V55() V56() V57() V58() V59() V60() cardinal limit_cardinal set
bool omega is V60() set
bool NAT is V60() set
K101(NAT) is V27() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT
0 is Relation-like non-zero 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 ext-real non positive non negative real V41() V42() complex-valued ext-real-valued real-valued natural-valued V53() V54() V55() V56() V57() V58() V59() V60() Function-yielding V70() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT
addcomplex is Relation-like Function-like V14([:COMPLEX,COMPLEX:]) V18([:COMPLEX,COMPLEX:], COMPLEX ) commutative associative having_a_unity complex-valued Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
multcomplex is Relation-like Function-like V14([:COMPLEX,COMPLEX:]) V18([:COMPLEX,COMPLEX:], COMPLEX ) commutative associative having_a_unity complex-valued Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
compreal is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
addreal is Relation-like Function-like V14([:REAL,REAL:]) V18([:REAL,REAL:], REAL ) commutative associative having_a_unity complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
diffreal is Relation-like Function-like V14([:REAL,REAL:]) V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
multreal is Relation-like Function-like V14([:REAL,REAL:]) V18([:REAL,REAL:], REAL ) commutative associative having_a_unity complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
the_unity_wrt addcomplex is complex Element of COMPLEX
the_unity_wrt addreal is complex ext-real real Element of REAL
the_unity_wrt multcomplex is complex Element of COMPLEX
the_unity_wrt multreal is complex ext-real real Element of REAL
card 0 is Relation-like non-zero 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 ext-real non positive non negative real V41() complex-valued ext-real-valued real-valued natural-valued V53() V54() V55() V56() V57() V58() V59() V60() Function-yielding V70() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered set
F is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V60() cardinal set
F |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on NAT
F -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V60() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = F } is set
Seg F is V53() V54() V55() V56() V57() V58() V60() F -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT : ( 1 <= b1 & b1 <= F ) } is set
(Seg F) --> 0 is Relation-like Seg F -defined Seg F -defined NAT -valued RAT -valued INT -valued Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{0}) complex-valued ext-real-valued real-valued natural-valued V60() Function-yielding V70() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{0}:]
{0} is functional non empty trivial V53() V54() V55() V56() V57() V58() 1 -element set
[:(Seg F),{0}:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:(Seg F),{0}:] is set
the Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
F is Relation-like complex-valued ext-real-valued real-valued set
rng F is V53() V54() V55() set
F is non empty set
[:REAL,F:] is Relation-like V60() set
bool [:REAL,F:] is V60() set
i is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
g is Relation-like Function-like non empty V14( REAL ) V18( REAL ,F) Element of bool [:REAL,F:]
i (#) g is Relation-like NAT -defined Function-like set
dom i is V53() V54() V55() V56() V57() V58() Element of bool NAT
j is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V60() cardinal set
Seg j is V53() V54() V55() V56() V57() V58() V60() j -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT : ( 1 <= b1 & b1 <= j ) } is set
dom (i (#) g) is V53() V54() V55() V56() V57() V58() set
dom g is non empty set
(i) is V53() V54() V55() Element of bool REAL
F is complex ext-real real set
<*F*> is Relation-like NAT -defined Function-like constant non empty trivial V60() 1 -element FinSequence-like FinSubsequence-like set
[1,F] is set
{1,F} is non empty V53() V54() V55() set
{1} is non empty trivial V53() V54() V55() V56() V57() V58() 1 -element set
{{1,F},{1}} is non empty set
{[1,F]} is Relation-like Function-like constant non empty trivial 1 -element set
g is complex ext-real real Element of REAL
<*g*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL
[1,g] is set
{1,g} is non empty V53() V54() V55() set
{{1,g},{1}} is non empty set
{[1,g]} is Relation-like Function-like constant non empty trivial 1 -element set
F is complex ext-real real set
g is complex ext-real real set
<*F,g*> is Relation-like NAT -defined Function-like non empty V60() 2 -element FinSequence-like FinSubsequence-like set
<*F*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,F] is set
{1,F} is non empty V53() V54() V55() set
{{1,F},{1}} is non empty set
{[1,F]} is Relation-like Function-like constant non empty trivial 1 -element set
<*g*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,g] is set
{1,g} is non empty V53() V54() V55() set
{{1,g},{1}} is non empty set
{[1,g]} is Relation-like Function-like constant non empty trivial 1 -element set
<*F*> ^ <*g*> is Relation-like NAT -defined Function-like non empty V60() 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT
i is complex ext-real real Element of REAL
j is complex ext-real real Element of REAL
<*i,j*> is Relation-like NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued V60() 2 -element FinSequence-like FinSubsequence-like FinSequence of REAL
<*i*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is set
{1,i} is non empty V53() V54() V55() set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*j*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,j] is set
{1,j} is non empty V53() V54() V55() set
{{1,j},{1}} is non empty set
{[1,j]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> ^ <*j*> is Relation-like NAT -defined Function-like non empty V60() 1 + 1 -element FinSequence-like FinSubsequence-like set
F is complex ext-real real set
g is complex ext-real real set
i is complex ext-real real set
<*F,g,i*> is Relation-like NAT -defined Function-like non empty V60() 3 -element FinSequence-like FinSubsequence-like set
<*F*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,F] is set
{1,F} is non empty V53() V54() V55() set
{{1,F},{1}} is non empty set
{[1,F]} is Relation-like Function-like constant non empty trivial 1 -element set
<*g*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,g] is set
{1,g} is non empty V53() V54() V55() set
{{1,g},{1}} is non empty set
{[1,g]} is Relation-like Function-like constant non empty trivial 1 -element set
<*F*> ^ <*g*> is Relation-like NAT -defined Function-like non empty V60() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*i*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is set
{1,i} is non empty V53() V54() V55() set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*F*> ^ <*g*>) ^ <*i*> is Relation-like NAT -defined Function-like non empty V60() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(1 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT
j is complex ext-real real Element of REAL
q2 is complex ext-real real Element of REAL
p3 is complex ext-real real Element of REAL
<*j,q2,p3*> is Relation-like NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued V60() 3 -element FinSequence-like FinSubsequence-like FinSequence of REAL
<*j*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,j] is set
{1,j} is non empty V53() V54() V55() set
{{1,j},{1}} is non empty set
{[1,j]} is Relation-like Function-like constant non empty trivial 1 -element set
<*q2*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,q2] is set
{1,q2} is non empty V53() V54() V55() set
{{1,q2},{1}} is non empty set
{[1,q2]} is Relation-like Function-like constant non empty trivial 1 -element set
<*j*> ^ <*q2*> is Relation-like NAT -defined Function-like non empty V60() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*p3*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,p3] is set
{1,p3} is non empty V53() V54() V55() set
{{1,p3},{1}} is non empty set
{[1,p3]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*j*> ^ <*q2*>) ^ <*p3*> is Relation-like NAT -defined Function-like non empty V60() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
F is complex ext-real real set
g is complex ext-real real set
i is complex ext-real real set
j is complex ext-real real set
<*F,g,i,j*> is Relation-like NAT -defined Function-like non empty V60() 4 -element FinSequence-like FinSubsequence-like set
<*F,g,i*> is Relation-like NAT -defined Function-like non empty complex-valued ext-real-valued real-valued V60() 3 -element FinSequence-like FinSubsequence-like set
<*F*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,F] is set
{1,F} is non empty V53() V54() V55() set
{{1,F},{1}} is non empty set
{[1,F]} is Relation-like Function-like constant non empty trivial 1 -element set
<*g*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,g] is set
{1,g} is non empty V53() V54() V55() set
{{1,g},{1}} is non empty set
{[1,g]} is Relation-like Function-like constant non empty trivial 1 -element set
<*F*> ^ <*g*> is Relation-like NAT -defined Function-like non empty V60() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*i*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is set
{1,i} is non empty V53() V54() V55() set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*F*> ^ <*g*>) ^ <*i*> is Relation-like NAT -defined Function-like non empty V60() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
<*j*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,j] is set
{1,j} is non empty V53() V54() V55() set
{{1,j},{1}} is non empty set
{[1,j]} is Relation-like Function-like constant non empty trivial 1 -element set
<*F,g,i*> ^ <*j*> is Relation-like NAT -defined Function-like non empty V60() 3 + 1 -element FinSequence-like FinSubsequence-like set
3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT
q2 is complex ext-real real Element of REAL
p3 is complex ext-real real Element of REAL
f3 is complex ext-real real Element of REAL
a is complex ext-real real Element of REAL
<*q2,p3,f3,a*> is Relation-like NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued V60() 4 -element FinSequence-like FinSubsequence-like FinSequence of REAL
<*q2,p3,f3*> is Relation-like NAT -defined Function-like non empty complex-valued ext-real-valued real-valued V60() 3 -element FinSequence-like FinSubsequence-like set
<*q2*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,q2] is set
{1,q2} is non empty V53() V54() V55() set
{{1,q2},{1}} is non empty set
{[1,q2]} is Relation-like Function-like constant non empty trivial 1 -element set
<*p3*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,p3] is set
{1,p3} is non empty V53() V54() V55() set
{{1,p3},{1}} is non empty set
{[1,p3]} is Relation-like Function-like constant non empty trivial 1 -element set
<*q2*> ^ <*p3*> is Relation-like NAT -defined Function-like non empty V60() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*f3*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,f3] is set
{1,f3} is non empty V53() V54() V55() set
{{1,f3},{1}} is non empty set
{[1,f3]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*q2*> ^ <*p3*>) ^ <*f3*> is Relation-like NAT -defined Function-like non empty V60() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
<*a*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V53() V54() V55() set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
<*q2,p3,f3*> ^ <*a*> is Relation-like NAT -defined Function-like non empty V60() 3 + 1 -element FinSequence-like FinSubsequence-like set
F is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V60() cardinal set
g is complex ext-real real set
F |-> g is Relation-like NAT -defined Function-like V60() F -element FinSequence-like FinSubsequence-like set
Seg F is V53() V54() V55() V56() V57() V58() V60() F -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT : ( 1 <= b1 & b1 <= F ) } is set
(Seg F) --> g is Relation-like Seg F -defined Seg F -defined Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{g}) complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{g}:]
{g} is non empty trivial V53() V54() V55() 1 -element set
[:(Seg F),{g}:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:(Seg F),{g}:] is set
F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
F ^ g is Relation-like NAT -defined Function-like V60() FinSequence-like FinSubsequence-like set
rng (F ^ g) is set
(F) is V53() V54() V55() Element of bool REAL
(g) is V53() V54() V55() Element of bool REAL
(F) \/ (g) is V53() V54() V55() set
id REAL is Relation-like REAL -defined REAL -valued Function-like one-to-one non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued V47() non-decreasing Element of bool [:REAL,REAL:]
addreal * ((id REAL),compreal) is Relation-like Function-like V14([:REAL,REAL:]) V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
F is Relation-like Function-like V14([:REAL,REAL:]) V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
g is complex ext-real real Element of REAL
i is complex ext-real real Element of REAL
diffreal . (g,i) is complex ext-real real Element of REAL
[g,i] is set
{g,i} is non empty V53() V54() V55() set
{g} is non empty trivial V53() V54() V55() 1 -element set
{{g,i},{g}} is non empty set
diffreal . [g,i] is complex ext-real real set
g - i is complex ext-real real Element of REAL
- i is complex ext-real real Element of REAL
g + (- i) is complex ext-real real Element of REAL
addreal . (g,(- i)) is complex ext-real real Element of REAL
[g,(- i)] is set
{g,(- i)} is non empty V53() V54() V55() set
{{g,(- i)},{g}} is non empty set
addreal . [g,(- i)] is complex ext-real real set
compreal . i is complex ext-real real Element of REAL
addreal . (g,(compreal . i)) is complex ext-real real Element of REAL
[g,(compreal . i)] is set
{g,(compreal . i)} is non empty V53() V54() V55() set
{{g,(compreal . i)},{g}} is non empty set
addreal . [g,(compreal . i)] is complex ext-real real set
(addreal * ((id REAL),compreal)) . (g,i) is complex ext-real real Element of REAL
(addreal * ((id REAL),compreal)) . [g,i] is complex ext-real real set
F is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g is complex ext-real real set
F . g is complex ext-real real Element of REAL
g ^2 is complex ext-real real set
g * g is complex ext-real real set
F is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
i is complex ext-real real Element of REAL
F . i is complex ext-real real Element of REAL
i ^2 is complex ext-real real Element of REAL
i * i is complex ext-real real set
g . i is complex ext-real real Element of REAL
() is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
F is complex ext-real real Element of REAL
g is complex ext-real real Element of REAL
i is complex ext-real real Element of REAL
addreal . (g,i) is complex ext-real real Element of REAL
[g,i] is set
{g,i} is non empty V53() V54() V55() set
{g} is non empty trivial V53() V54() V55() 1 -element set
{{g,i},{g}} is non empty set
addreal . [g,i] is complex ext-real real set
multreal . (F,(addreal . (g,i))) is complex ext-real real Element of REAL
[F,(addreal . (g,i))] is set
{F,(addreal . (g,i))} is non empty V53() V54() V55() set
{F} is non empty trivial V53() V54() V55() 1 -element set
{{F,(addreal . (g,i))},{F}} is non empty set
multreal . [F,(addreal . (g,i))] is complex ext-real real set
g + i is complex ext-real real Element of REAL
multreal . (F,(g + i)) is complex ext-real real Element of REAL
[F,(g + i)] is set
{F,(g + i)} is non empty V53() V54() V55() set
{{F,(g + i)},{F}} is non empty set
multreal . [F,(g + i)] is complex ext-real real set
F * (g + i) is complex ext-real real Element of REAL
F * g is complex ext-real real Element of REAL
F * i is complex ext-real real Element of REAL
(F * g) + (F * i) is complex ext-real real Element of REAL
addreal . ((F * g),(F * i)) is complex ext-real real Element of REAL
[(F * g),(F * i)] is set
{(F * g),(F * i)} is non empty V53() V54() V55() set
{(F * g)} is non empty trivial V53() V54() V55() 1 -element set
{{(F * g),(F * i)},{(F * g)}} is non empty set
addreal . [(F * g),(F * i)] is complex ext-real real set
multreal . (F,g) is complex ext-real real Element of REAL
[F,g] is set
{F,g} is non empty V53() V54() V55() set
{{F,g},{F}} is non empty set
multreal . [F,g] is complex ext-real real set
addreal . ((multreal . (F,g)),(F * i)) is complex ext-real real Element of REAL
[(multreal . (F,g)),(F * i)] is set
{(multreal . (F,g)),(F * i)} is non empty V53() V54() V55() set
{(multreal . (F,g))} is non empty trivial V53() V54() V55() 1 -element set
{{(multreal . (F,g)),(F * i)},{(multreal . (F,g))}} is non empty set
addreal . [(multreal . (F,g)),(F * i)] is complex ext-real real set
multreal . (F,i) is complex ext-real real Element of REAL
[F,i] is set
{F,i} is non empty V53() V54() V55() set
{{F,i},{F}} is non empty set
multreal . [F,i] is complex ext-real real set
addreal . ((multreal . (F,g)),(multreal . (F,i))) is complex ext-real real Element of REAL
[(multreal . (F,g)),(multreal . (F,i))] is set
{(multreal . (F,g)),(multreal . (F,i))} is non empty V53() V54() V55() set
{{(multreal . (F,g)),(multreal . (F,i))},{(multreal . (F,g))}} is non empty set
addreal . [(multreal . (F,g)),(multreal . (F,i))] is complex ext-real real set
addreal . (F,g) is complex ext-real real Element of REAL
addreal . [F,g] is complex ext-real real set
multreal . ((addreal . (F,g)),i) is complex ext-real real Element of REAL
[(addreal . (F,g)),i] is set
{(addreal . (F,g)),i} is non empty V53() V54() V55() set
{(addreal . (F,g))} is non empty trivial V53() V54() V55() 1 -element set
{{(addreal . (F,g)),i},{(addreal . (F,g))}} is non empty set
multreal . [(addreal . (F,g)),i] is complex ext-real real set
F + g is complex ext-real real Element of REAL
multreal . ((F + g),i) is complex ext-real real Element of REAL
[(F + g),i] is set
{(F + g),i} is non empty V53() V54() V55() set
{(F + g)} is non empty trivial V53() V54() V55() 1 -element set
{{(F + g),i},{(F + g)}} is non empty set
multreal . [(F + g),i] is complex ext-real real set
(F + g) * i is complex ext-real real Element of REAL
g * i is complex ext-real real Element of REAL
(F * i) + (g * i) is complex ext-real real Element of REAL
addreal . ((F * i),(g * i)) is complex ext-real real Element of REAL
[(F * i),(g * i)] is set
{(F * i),(g * i)} is non empty V53() V54() V55() set
{(F * i)} is non empty trivial V53() V54() V55() 1 -element set
{{(F * i),(g * i)},{(F * i)}} is non empty set
addreal . [(F * i),(g * i)] is complex ext-real real set
addreal . ((multreal . (F,i)),(g * i)) is complex ext-real real Element of REAL
[(multreal . (F,i)),(g * i)] is set
{(multreal . (F,i)),(g * i)} is non empty V53() V54() V55() set
{(multreal . (F,i))} is non empty trivial V53() V54() V55() 1 -element set
{{(multreal . (F,i)),(g * i)},{(multreal . (F,i))}} is non empty set
addreal . [(multreal . (F,i)),(g * i)] is complex ext-real real set
multreal . (g,i) is complex ext-real real Element of REAL
multreal . [g,i] is complex ext-real real set
addreal . ((multreal . (F,i)),(multreal . (g,i))) is complex ext-real real Element of REAL
[(multreal . (F,i)),(multreal . (g,i))] is set
{(multreal . (F,i)),(multreal . (g,i))} is non empty V53() V54() V55() set
{{(multreal . (F,i)),(multreal . (g,i))},{(multreal . (F,i))}} is non empty set
addreal . [(multreal . (F,i)),(multreal . (g,i))] is complex ext-real real set
F is complex ext-real real Element of REAL
() . F is complex ext-real real Element of REAL
g is complex ext-real real Element of REAL
multreal . (F,g) is complex ext-real real Element of REAL
[F,g] is set
{F,g} is non empty V53() V54() V55() set
{F} is non empty trivial V53() V54() V55() 1 -element set
{{F,g},{F}} is non empty set
multreal . [F,g] is complex ext-real real set
() . (multreal . (F,g)) is complex ext-real real Element of REAL
() . g is complex ext-real real Element of REAL
multreal . ((() . F),(() . g)) is complex ext-real real Element of REAL
[(() . F),(() . g)] is set
{(() . F),(() . g)} is non empty V53() V54() V55() set
{(() . F)} is non empty trivial V53() V54() V55() 1 -element set
{{(() . F),(() . g)},{(() . F)}} is non empty set
multreal . [(() . F),(() . g)] is complex ext-real real set
multreal . (F,g) is complex ext-real real Element of REAL
() . (multreal . (F,g)) is complex ext-real real Element of REAL
F * g is complex ext-real real Element of REAL
() . (F * g) is complex ext-real real Element of REAL
(F * g) ^2 is complex ext-real real Element of REAL
(F * g) * (F * g) is complex ext-real real set
F ^2 is complex ext-real real Element of REAL
F * F is complex ext-real real set
g ^2 is complex ext-real real Element of REAL
g * g is complex ext-real real set
(F ^2) * (g ^2) is complex ext-real real Element of REAL
multreal . ((F ^2),(g ^2)) is complex ext-real real Element of REAL
[(F ^2),(g ^2)] is set
{(F ^2),(g ^2)} is non empty V53() V54() V55() set
{(F ^2)} is non empty trivial V53() V54() V55() 1 -element set
{{(F ^2),(g ^2)},{(F ^2)}} is non empty set
multreal . [(F ^2),(g ^2)] is complex ext-real real set
() . F is complex ext-real real Element of REAL
multreal . ((() . F),(g ^2)) is complex ext-real real Element of REAL
[(() . F),(g ^2)] is set
{(() . F),(g ^2)} is non empty V53() V54() V55() set
{(() . F)} is non empty trivial V53() V54() V55() 1 -element set
{{(() . F),(g ^2)},{(() . F)}} is non empty set
multreal . [(() . F),(g ^2)] is complex ext-real real set
() . g is complex ext-real real Element of REAL
multreal . ((() . F),(() . g)) is complex ext-real real Element of REAL
[(() . F),(() . g)] is set
{(() . F),(() . g)} is non empty V53() V54() V55() set
{{(() . F),(() . g)},{(() . F)}} is non empty set
multreal . [(() . F),(() . g)] is complex ext-real real set
F is complex ext-real real set
multreal [;] (F,(id REAL)) is Relation-like Function-like set
g is complex ext-real real Element of REAL
multreal [;] (g,(id REAL)) is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
F is complex ext-real real set
multreal [;] (F,(id REAL)) is Relation-like Function-like set
g is complex ext-real real set
(multreal [;] (F,(id REAL))) . g is set
F * g is complex ext-real real Element of REAL
i is complex ext-real real Element of REAL
j is complex ext-real real Element of REAL
(id REAL) . j is complex ext-real real Element of REAL
multreal . (i,((id REAL) . j)) is complex ext-real real Element of REAL
[i,((id REAL) . j)] is set
{i,((id REAL) . j)} is non empty V53() V54() V55() set
{i} is non empty trivial V53() V54() V55() 1 -element set
{{i,((id REAL) . j)},{i}} is non empty set
multreal . [i,((id REAL) . j)] is complex ext-real real set
multreal . (i,j) is complex ext-real real Element of REAL
[i,j] is set
{i,j} is non empty V53() V54() V55() set
{{i,j},{i}} is non empty set
multreal . [i,j] is complex ext-real real set
F is complex ext-real real set
(F) is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
multreal [;] (F,(id REAL)) is Relation-like Function-like set
g is complex ext-real real set
(F) . g is complex ext-real real Element of REAL
F * g is complex ext-real real Element of REAL
F is complex ext-real real set
(F) is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
multreal [;] (F,(id REAL)) is Relation-like Function-like set
F is complex ext-real real Element of REAL
compreal . F is complex ext-real real Element of REAL
addreal . (F,(compreal . F)) is complex ext-real real Element of REAL
[F,(compreal . F)] is set
{F,(compreal . F)} is non empty V53() V54() V55() set
{F} is non empty trivial V53() V54() V55() 1 -element set
{{F,(compreal . F)},{F}} is non empty set
addreal . [F,(compreal . F)] is complex ext-real real set
addreal . ((compreal . F),F) is complex ext-real real Element of REAL
[(compreal . F),F] is set
{(compreal . F),F} is non empty V53() V54() V55() set
{(compreal . F)} is non empty trivial V53() V54() V55() 1 -element set
{{(compreal . F),F},{(compreal . F)}} is non empty set
addreal . [(compreal . F),F] is complex ext-real real set
compreal . F is complex ext-real real Element of REAL
addreal . (F,(compreal . F)) is complex ext-real real Element of REAL
[F,(compreal . F)] is set
{F,(compreal . F)} is non empty V53() V54() V55() set
{{F,(compreal . F)},{F}} is non empty set
addreal . [F,(compreal . F)] is complex ext-real real set
F + (compreal . F) is complex ext-real real Element of REAL
- F is complex ext-real real Element of REAL
F + (- F) is complex ext-real real Element of REAL
addreal . ((compreal . F),F) is complex ext-real real Element of REAL
[(compreal . F),F] is set
{(compreal . F),F} is non empty V53() V54() V55() set
{(compreal . F)} is non empty trivial V53() V54() V55() 1 -element set
{{(compreal . F),F},{(compreal . F)}} is non empty set
addreal . [(compreal . F),F] is complex ext-real real set
(compreal . F) + F is complex ext-real real Element of REAL
(- F) + F is complex ext-real real Element of REAL
the_inverseOp_wrt addreal is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
(F) is V53() V54() V55() Element of bool REAL
F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
F + g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
addreal .: (F,g) is Relation-like Function-like set
q2 is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
dom addreal is set
i is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
(i) is V53() V54() V55() Element of bool REAL
j is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
(j) is V53() V54() V55() Element of bool REAL
[:(i),(j):] is Relation-like complex-valued ext-real-valued real-valued set
dom (addreal .: (F,g)) is set
dom F is V53() V54() V55() V56() V57() V58() Element of bool NAT
dom g is V53() V54() V55() V56() V57() V58() Element of bool NAT
(dom F) /\ (dom g) is V53() V54() V55() V56() V57() V58() set
dom (F + g) is V53() V54() V55() V56() V57() V58() Element of bool NAT
p3 is set
q2 . p3 is complex ext-real real Element of REAL
F . p3 is complex ext-real real Element of REAL
g . p3 is complex ext-real real Element of REAL
addreal . ((F . p3),(g . p3)) is complex ext-real real Element of REAL
[(F . p3),(g . p3)] is set
{(F . p3),(g . p3)} is non empty V53() V54() V55() set
{(F . p3)} is non empty trivial V53() V54() V55() 1 -element set
{{(F . p3),(g . p3)},{(F . p3)}} is non empty set
addreal . [(F . p3),(g . p3)] is complex ext-real real set
(F . p3) + (g . p3) is complex ext-real real Element of REAL
p3 is set
dom q2 is V53() V54() V55() V56() V57() V58() Element of bool NAT
q2 . p3 is complex ext-real real Element of REAL
F . p3 is complex ext-real real Element of REAL
g . p3 is complex ext-real real Element of REAL
addreal . ((F . p3),(g . p3)) is complex ext-real real Element of REAL
[(F . p3),(g . p3)] is set
{(F . p3),(g . p3)} is non empty V53() V54() V55() set
{(F . p3)} is non empty trivial V53() V54() V55() 1 -element set
{{(F . p3),(g . p3)},{(F . p3)}} is non empty set
addreal . [(F . p3),(g . p3)] is complex ext-real real set
(F . p3) + (g . p3) is complex ext-real real Element of REAL
i is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
j is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
q2 is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
addreal .: (j,q2) is Relation-like Function-like set
addreal .: (q2,j) is Relation-like Function-like set
dom addreal is set
f3 is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
(f3) is V53() V54() V55() Element of bool REAL
p3 is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
(p3) is V53() V54() V55() Element of bool REAL
[:(f3),(p3):] is Relation-like complex-valued ext-real-valued real-valued set
[:(p3),(f3):] is Relation-like complex-valued ext-real-valued real-valued set
addreal .: (p3,f3) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
dom (addreal .: (p3,f3)) is V53() V54() V55() V56() V57() V58() Element of bool NAT
dom p3 is V53() V54() V55() V56() V57() V58() Element of bool NAT
dom f3 is V53() V54() V55() V56() V57() V58() Element of bool NAT
(dom p3) /\ (dom f3) is V53() V54() V55() V56() V57() V58() set
addreal .: (f3,p3) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
dom (addreal .: (f3,p3)) is V53() V54() V55() V56() V57() V58() Element of bool NAT
a is set
i . a is complex ext-real real Element of REAL
f3 . a is complex ext-real real Element of REAL
p3 . a is complex ext-real real Element of REAL
addreal . ((f3 . a),(p3 . a)) is complex ext-real real Element of REAL
[(f3 . a),(p3 . a)] is set
{(f3 . a),(p3 . a)} is non empty V53() V54() V55() set
{(f3 . a)} is non empty trivial V53() V54() V55() 1 -element set
{{(f3 . a),(p3 . a)},{(f3 . a)}} is non empty set
addreal . [(f3 . a),(p3 . a)] is complex ext-real real set
addreal . ((p3 . a),(f3 . a)) is complex ext-real real Element of REAL
[(p3 . a),(f3 . a)] is set
{(p3 . a),(f3 . a)} is non empty V53() V54() V55() set
{(p3 . a)} is non empty trivial V53() V54() V55() 1 -element set
{{(p3 . a),(f3 . a)},{(p3 . a)}} is non empty set
addreal . [(p3 . a),(f3 . a)] is complex ext-real real set
(p3 . a) + (f3 . a) is complex ext-real real Element of REAL
F is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V60() cardinal set
F -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V60() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = F } is set
g is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL
i is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL
g + i is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
addreal .: (g,i) is Relation-like Function-like set
F is set
g is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V60() cardinal set
g -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V60() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = g } is set
i is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() g -element FinSequence-like FinSubsequence-like Element of g -tuples_on REAL
i . F is complex ext-real real Element of REAL
j is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() g -element FinSequence-like FinSubsequence-like Element of g -tuples_on REAL
(g,i,j) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() g -element FinSequence-like FinSubsequence-like Element of g -tuples_on REAL
addreal .: (i,j) is Relation-like Function-like set
(g,i,j) . F is complex ext-real real Element of REAL
j . F is complex ext-real real Element of REAL
(i . F) + (j . F) is complex ext-real real Element of REAL
Seg g is V53() V54() V55() V56() V57() V58() V60() g -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT : ( 1 <= b1 & b1 <= g ) } is set
dom j is V53() V54() V55() V56() V57() V58() g -element Element of bool NAT
dom i is V53() V54() V55() V56() V57() V58() g -element Element of bool NAT
dom (g,i,j) is V53() V54() V55() V56() V57() V58() g -element Element of bool NAT
0 + 0 is Relation-like non-zero 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 ext-real non positive non negative real V41() V42() complex-valued ext-real-valued real-valued natural-valued V53() V54() V55() V56() V57() V58() V59() V60() Function-yielding V70() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
(i . F) + 0 is complex ext-real real Element of REAL
Seg g is V53() V54() V55() V56() V57() V58() V60() g -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT : ( 1 <= b1 & b1 <= g ) } is set
dom (g,i,j) is V53() V54() V55() V56() V57() V58() g -element Element of bool NAT
Seg g is V53() V54() V55() V56() V57() V58() V60() g -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT : ( 1 <= b1 & b1 <= g ) } is set
<*> REAL is Relation-like non-zero empty-yielding NAT -defined REAL -valued RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V41() complex-valued ext-real-valued real-valued natural-valued V53() V54() V55() V56() V57() V58() V59() V60() Function-yielding V70() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of REAL
F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
((<*> REAL),F) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
addreal .: ((<*> REAL),F) is Relation-like Function-like set
F is complex ext-real real set
<*F*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,F] is set
{1,F} is non empty V53() V54() V55() set
{{1,F},{1}} is non empty set
{[1,F]} is Relation-like Function-like constant non empty trivial 1 -element set
g is complex ext-real real set
<*g*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set
[1,g] is set
{1,g} is non empty V53() V54() V55() set
{{1,g},{1}} is non empty set
{[1,g]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*F*>,<*g*>) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
addreal .: (<*F*>,<*g*>) is Relation-like Function-like set
F + g is complex ext-real real Element of REAL
<*(F + g)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL
[1,(F + g)] is set
{1,(F + g)} is non empty V53() V54() V55() set
{{1,(F + g)},{1}} is non empty set
{[1,(F + g)]} is Relation-like Function-like constant non empty trivial 1 -element set
i is complex ext-real real Element of REAL
<*i*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL
[1,i] is set
{1,i} is non empty V53() V54() V55() set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
j is complex ext-real real Element of REAL
<*j*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL
[1,j] is set
{1,j} is non empty V53() V54() V55() set
{{1,j},{1}} is non empty set
{[1,j]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*i*>,<*j*>) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
addreal .: (<*i*>,<*j*>) is Relation-like Function-like set
addreal . (i,j) is complex ext-real real Element of REAL
[i,j] is set
{i,j} is non empty V53() V54() V55() set
{i} is non empty trivial V53() V54() V55() 1 -element set
{{i,j},{i}} is non empty set
addreal . [i,j] is complex ext-real real set
<*(addreal . (i,j))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL
[1,(addreal . (i,j))] is set
{1,(addreal . (i,j))} is non empty V53() V54() V55() set
{{1,(addreal . (i,j))},{1}} is non empty set
{[1,(addreal . (i,j))]} is Relation-like Function-like constant non empty trivial 1 -element set
F is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V60() cardinal set
g is complex ext-real real set
F |-> g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like set
Seg F is V53() V54() V55() V56() V57() V58() V60() F -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT : ( 1 <= b1 & b1 <= F ) } is set
(Seg F) --> g is Relation-like Seg F -defined Seg F -defined Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{g}) complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{g}:]
{g} is non empty trivial V53() V54() V55() 1 -element set
[:(Seg F),{g}:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:(Seg F),{g}:] is set
i is complex ext-real real set
F |-> i is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like set
(Seg F) --> i is Relation-like Seg F -defined Seg F -defined Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{i}) complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{i}:]
{i} is non empty trivial V53() V54() V55() 1 -element set
[:(Seg F),{i}:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:(Seg F),{i}:] is set
((F |-> g),(F |-> i)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
addreal .: ((F |-> g),(F |-> i)) is Relation-like Function-like set
g + i is complex ext-real real Element of REAL
F |-> (g + i) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL
F -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V60() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = F } is set
(Seg F) --> (g + i) is Relation-like Seg F -defined Seg F -defined REAL -valued Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{(g + i)}) complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{(g + i)}:]
{(g + i)} is non empty trivial V53() V54() V55() 1 -element set
[:(Seg F),{(g + i)}:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:(Seg F),{(g + i)}:] is set
j is complex ext-real real Element of REAL
F |-> j is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL
(Seg F) --> j is Relation-like Seg F -defined Seg F -defined REAL -valued Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{j}) complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{j}:]
{j} is non empty trivial V53() V54() V55() 1 -element set
[:(Seg F),{j}:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:(Seg F),{j}:] is set
q2 is complex ext-real real Element of REAL
F |-> q2 is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL
(Seg F) --> q2 is Relation-like Seg F -defined Seg F -defined REAL -valued Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{q2}) complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{q2}:]
{q2} is non empty trivial V53() V54() V55() 1 -element set
[:(Seg F),{q2}:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:(Seg F),{q2}:] is set
(F,(F |-> j),(F |-> q2)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL
addreal .: ((F |-> j),(F |-> q2)) is Relation-like Function-like set
addreal . (j,q2) is complex ext-real real Element of REAL
[j,q2] is set
{j,q2} is non empty V53() V54() V55() set
{{j,q2},{j}} is non empty set
addreal . [j,q2] is complex ext-real real set
F |-> (addreal . (j,q2)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL
(Seg F) --> (addreal . (j,q2)) is Relation-like Seg F -defined Seg F -defined REAL -valued Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{(addreal . (j,q2))}) complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{(addreal . (j,q2))}:]
{(addreal . (j,q2))} is non empty trivial V53() V54() V55() 1 -element set
[:(Seg F),{(addreal . (j,q2))}:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:(Seg F),{(addreal . (j,q2))}:] is set
F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
i is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
(g,i) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
addreal .: (g,i) is Relation-like Function-like set
(F,(g,i)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
addreal .: (F,(g,i)) is Relation-like Function-like set
(F,g) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
addreal .: (F,g) is Relation-like Function-like set
((F,g),i) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL
addreal .: ((F,g),i) is Relation-like Function-like set
F is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V60() cardinal set
F -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V60() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = F } is set
g is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL
F |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL
Seg F is V53() V54() V55() V56() V57() V58() V60() F -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT : ( 1 <= b1 & b1 <= F ) } is set
(Seg F) --> 0 is Relation-like Seg F -defined Seg F -defined NAT -valued RAT -valued INT -valued Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{0}) complex-valued ext-real-valued real-valued natural-valued V60() Function-yielding V70() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{0}:]
{0} is functional non empty trivial V53() V54() V55() V56() V57() V58() 1 -element set
[:(Seg F),{0}:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:(Seg F),{0}:] is set
(F,g,(F |-> 0)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL
addreal .: (g,(F |-> 0)) is Relation-like Function-like set
g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
- g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
- 1 is non empty complex ext-real non positive negative real V41() set
(- 1) (#) g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
F is set
(- g) . F is complex ext-real real Element of REAL
g . F is complex ext-real real Element of REAL
- (g . F) is complex ext-real real Element of REAL
F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
- F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
- 1 is non empty complex ext-real non positive negative real V41() set
(- 1) (#) F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set
F (#) compreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set