REAL is non empty V45() V67() V68() V69() V73() set
NAT is ordinal V45() cardinal limit_cardinal V67() V68() V69() V70() V71() V72() V73() Element of bool REAL
bool REAL is V45() set
COMPLEX is non empty V45() V67() V73() set
RAT is non empty V45() V67() V68() V69() V70() V73() set
0 is set
the Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ordinal natural complex real V38() Function-yielding V44() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V67() V68() V69() V70() V71() V72() V73() set is Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ordinal natural complex real V38() Function-yielding V44() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V67() V68() V69() V70() V71() V72() V73() set
INT is non empty V45() V67() V68() V69() V70() V71() V73() set
[:COMPLEX,COMPLEX:] is Relation-like V45() complex-valued set
bool [:COMPLEX,COMPLEX:] is V45() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like V45() complex-valued set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is V45() set
[:REAL,REAL:] is Relation-like V45() complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is V45() set
[:[:REAL,REAL:],REAL:] is Relation-like V45() complex-valued ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is V45() set
[:RAT,RAT:] is Relation-like RAT -valued V45() complex-valued ext-real-valued real-valued set
bool [:RAT,RAT:] is V45() set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued V45() complex-valued ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is V45() set
[:INT,INT:] is Relation-like RAT -valued INT -valued V45() complex-valued ext-real-valued real-valued set
bool [:INT,INT:] is V45() set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued V45() complex-valued ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is V45() set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is set
omega is ordinal V45() cardinal limit_cardinal V67() V68() V69() V70() V71() V72() V73() set
bool omega is V45() set
bool NAT is V45() set
K138(NAT) is V36() set
[:COMPLEX,REAL:] is Relation-like V45() complex-valued ext-real-valued real-valued set
bool [:COMPLEX,REAL:] is V45() set
1 is non empty ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
2 is non empty ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
3 is non empty ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
0 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
compcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
addcomplex is Relation-like Function-like V14([:COMPLEX,COMPLEX:]) V18([:COMPLEX,COMPLEX:], COMPLEX ) commutative associative V37( COMPLEX ) complex-valued Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
diffcomplex is Relation-like Function-like V14([:COMPLEX,COMPLEX:]) V18([:COMPLEX,COMPLEX:], COMPLEX ) complex-valued Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
id COMPLEX is Relation-like COMPLEX -defined COMPLEX -valued Function-like one-to-one non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
addcomplex * ((id COMPLEX),compcomplex) is Relation-like Function-like V14([:COMPLEX,COMPLEX:]) V18([:COMPLEX,COMPLEX:], COMPLEX ) complex-valued Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
multcomplex is Relation-like Function-like V14([:COMPLEX,COMPLEX:]) V18([:COMPLEX,COMPLEX:], COMPLEX ) commutative associative V37( COMPLEX ) complex-valued Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
the_unity_wrt addcomplex is complex Element of COMPLEX
the_unity_wrt multcomplex is complex Element of COMPLEX
K265(COMPLEX,addcomplex) is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
x is Relation-like complex-valued set
rng x is V67() set
bool COMPLEX is V45() set
x is non empty set
[:COMPLEX,x:] is Relation-like V45() set
bool [:COMPLEX,x:] is V45() set
z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX ,x) Element of bool [:COMPLEX,x:]
z (#) y is Relation-like NAT -defined Function-like set
dom z is V67() V68() V69() V70() V71() V72() Element of bool NAT
x2 is ordinal natural complex real V38() V45() cardinal set
Seg x2 is V45() x2 -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x2) ) } is set
dom (z (#) y) is V67() V68() V69() V70() V71() V72() set
dom y is non empty set
(z) is V67() Element of bool COMPLEX
x is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
y is complex set
x . y is complex set
y ^2 is set
y * y is set
x is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
y is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
z is complex Element of COMPLEX
x . z is complex Element of COMPLEX
z ^2 is complex Element of COMPLEX
z * z is set
y . z is complex Element of COMPLEX
() is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
x is complex Element of COMPLEX
() . x is complex Element of COMPLEX
y is complex Element of COMPLEX
multcomplex . (x,y) is complex Element of COMPLEX
[x,y] is set
{x,y} is V67() set
{x} is non empty trivial 1 -element V67() set
{{x,y},{x}} is set
multcomplex . [x,y] is complex set
() . (multcomplex . (x,y)) is complex Element of COMPLEX
() . y is complex Element of COMPLEX
multcomplex . ((() . x),(() . y)) is complex Element of COMPLEX
[(() . x),(() . y)] is set
{(() . x),(() . y)} is V67() set
{(() . x)} is non empty trivial 1 -element V67() set
{{(() . x),(() . y)},{(() . x)}} is set
multcomplex . [(() . x),(() . y)] is complex set
multcomplex . (x,y) is complex Element of COMPLEX
() . (multcomplex . (x,y)) is complex Element of COMPLEX
x * y is complex Element of COMPLEX
() . (x * y) is complex Element of COMPLEX
(x * y) ^2 is complex Element of COMPLEX
(x * y) * (x * y) is set
x ^2 is complex Element of COMPLEX
x * x is set
y ^2 is complex Element of COMPLEX
y * y is set
(x ^2) * (y ^2) is complex Element of COMPLEX
multcomplex . ((x ^2),(y ^2)) is complex Element of COMPLEX
[(x ^2),(y ^2)] is set
{(x ^2),(y ^2)} is V67() set
{(x ^2)} is non empty trivial 1 -element V67() set
{{(x ^2),(y ^2)},{(x ^2)}} is set
multcomplex . [(x ^2),(y ^2)] is complex set
multcomplex . ((() . x),(y ^2)) is complex Element of COMPLEX
[(() . x),(y ^2)] is set
{(() . x),(y ^2)} is V67() set
{{(() . x),(y ^2)},{(() . x)}} is set
multcomplex . [(() . x),(y ^2)] is complex set
multcomplex . ((() . x),(() . y)) is complex Element of COMPLEX
x is complex set
multcomplex [;] (x,(id COMPLEX)) is Relation-like Function-like set
y is complex set
(multcomplex [;] (x,(id COMPLEX))) . y is set
x * y is complex Element of COMPLEX
z is complex Element of COMPLEX
x2 is complex Element of COMPLEX
(id COMPLEX) . x2 is complex Element of COMPLEX
multcomplex . (z,((id COMPLEX) . x2)) is complex Element of COMPLEX
[z,((id COMPLEX) . x2)] is set
{z,((id COMPLEX) . x2)} is V67() set
{z} is non empty trivial 1 -element V67() set
{{z,((id COMPLEX) . x2)},{z}} is set
multcomplex . [z,((id COMPLEX) . x2)] is complex set
multcomplex . (z,x2) is complex Element of COMPLEX
[z,x2] is set
{z,x2} is V67() set
{{z,x2},{z}} is set
multcomplex . [z,x2] is complex set
x is complex set
x multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (x,(id COMPLEX)) is Relation-like Function-like set
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(x) is V67() Element of bool COMPLEX
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x + y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (x,y) is Relation-like Function-like set
y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
dom addcomplex is set
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(z) is V67() Element of bool COMPLEX
x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x2) is V67() Element of bool COMPLEX
[:(z),(x2):] is Relation-like complex-valued set
dom (addcomplex .: (x,y)) is set
dom x is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom y is V67() V68() V69() V70() V71() V72() Element of bool NAT
(dom x) /\ (dom y) is V67() V68() V69() V70() V71() V72() set
dom (x + y) is V67() V68() V69() V70() V71() V72() Element of bool NAT
z2 is set
y2 . z2 is complex set
x . z2 is complex set
y . z2 is complex set
addcomplex . ((x . z2),(y . z2)) is set
[(x . z2),(y . z2)] is set
{(x . z2),(y . z2)} is V67() set
{(x . z2)} is non empty trivial 1 -element V67() set
{{(x . z2),(y . z2)},{(x . z2)}} is set
addcomplex . [(x . z2),(y . z2)] is complex set
(x . z2) + (y . z2) is complex Element of COMPLEX
z2 is set
dom y2 is V67() V68() V69() V70() V71() V72() Element of bool NAT
y2 . z2 is complex set
x . z2 is complex set
y . z2 is complex set
addcomplex . ((x . z2),(y . z2)) is set
[(x . z2),(y . z2)] is set
{(x . z2),(y . z2)} is V67() set
{(x . z2)} is non empty trivial 1 -element V67() set
{{(x . z2),(y . z2)},{(x . z2)}} is set
addcomplex . [(x . z2),(y . z2)] is complex set
(x . z2) + (y . z2) is complex Element of COMPLEX
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
x2 is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y2 is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (x2,y2) is Relation-like Function-like set
addcomplex .: (y2,x2) is Relation-like Function-like set
dom addcomplex is set
i is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(i) is V67() Element of bool COMPLEX
z2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(z2) is V67() Element of bool COMPLEX
[:(i),(z2):] is Relation-like complex-valued set
[:(z2),(i):] is Relation-like complex-valued set
addcomplex .: (z2,i) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
dom (addcomplex .: (z2,i)) is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom z2 is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom i is V67() V68() V69() V70() V71() V72() Element of bool NAT
(dom z2) /\ (dom i) is V67() V68() V69() V70() V71() V72() set
addcomplex .: (i,z2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
dom (addcomplex .: (i,z2)) is V67() V68() V69() V70() V71() V72() Element of bool NAT
a is set
z . a is complex set
i . a is complex set
z2 . a is complex set
addcomplex . ((i . a),(z2 . a)) is set
[(i . a),(z2 . a)] is set
{(i . a),(z2 . a)} is V67() set
{(i . a)} is non empty trivial 1 -element V67() set
{{(i . a),(z2 . a)},{(i . a)}} is set
addcomplex . [(i . a),(z2 . a)] is complex set
addcomplex . ((z2 . a),(i . a)) is set
[(z2 . a),(i . a)] is set
{(z2 . a),(i . a)} is V67() set
{(z2 . a)} is non empty trivial 1 -element V67() set
{{(z2 . a),(i . a)},{(z2 . a)}} is set
addcomplex . [(z2 . a),(i . a)] is complex set
(z2 . a) + (i . a) is complex Element of COMPLEX
x is ordinal natural complex real V38() V45() cardinal set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
y + z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (y,z) is Relation-like Function-like set
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
COMPLEX * is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
x is set
y is ordinal natural complex real V38() V45() cardinal set
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() y -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z . x is complex set
x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() y -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(y,z,x2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() y -element FinSequence-like FinSubsequence-like complex-valued Element of y -tuples_on COMPLEX
y -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = y } is set
addcomplex .: (z,x2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (z,x2) is Relation-like Function-like set
(y,z,x2) . x is complex set
x2 . x is complex set
(z . x) + (x2 . x) is complex Element of COMPLEX
Seg y is V45() y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,y) ) } is set
dom x2 is y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
dom z is y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
dom (y,z,x2) is y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
0 + 0 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
(z . x) + 0 is complex Element of COMPLEX
Seg y is V45() y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,y) ) } is set
dom (y,z,x2) is y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
Seg y is V45() y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,y) ) } is set
<*> COMPLEX is Relation-like non-zero empty-yielding NAT -defined COMPLEX -valued RAT -valued Function-like one-to-one constant functional empty ordinal natural complex real V38() Function-yielding V44() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V67() V68() V69() V70() V71() V72() V73() FinSequence of COMPLEX
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((<*> COMPLEX),x) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((<*> COMPLEX),x) is Relation-like Function-like set
x is complex set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,x] is set
{1,x} is V67() set
{1} is non empty trivial 1 -element V67() V68() V69() V70() V71() V72() set
{{1,x},{1}} is set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
y is complex set
<*y*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,y] is set
{1,y} is V67() set
{{1,y},{1}} is set
{[1,y]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*x*>,<*y*>) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (<*x*>,<*y*>) is Relation-like Function-like set
x + y is complex Element of COMPLEX
<*(x + y)*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,(x + y)] is set
{1,(x + y)} is V67() set
{{1,(x + y)},{1}} is set
{[1,(x + y)]} is Relation-like Function-like constant non empty trivial 1 -element set
z is complex Element of COMPLEX
<*z*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,z] is set
{1,z} is V67() set
{{1,z},{1}} is set
{[1,z]} is Relation-like Function-like constant non empty trivial 1 -element set
x2 is complex Element of COMPLEX
<*x2*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,x2] is set
{1,x2} is V67() set
{{1,x2},{1}} is set
{[1,x2]} is Relation-like Function-like constant non empty trivial 1 -element set
(1,<*z*>,<*x2*>) is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued Element of 1 -tuples_on COMPLEX
1 -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = 1 } is set
addcomplex .: (<*z*>,<*x2*>) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (<*z*>,<*x2*>) is Relation-like Function-like set
addcomplex . (z,x2) is complex Element of COMPLEX
[z,x2] is set
{z,x2} is V67() set
{z} is non empty trivial 1 -element V67() set
{{z,x2},{z}} is set
addcomplex . [z,x2] is complex set
<*(addcomplex . (z,x2))*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,(addcomplex . (z,x2))] is set
{1,(addcomplex . (z,x2))} is V67() set
{{1,(addcomplex . (z,x2))},{1}} is set
{[1,(addcomplex . (z,x2))]} is Relation-like Function-like constant non empty trivial 1 -element set
x is ordinal natural complex real V38() V45() cardinal set
y is complex set
x |-> y is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> y is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{y}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{y}:]
{y} is non empty trivial 1 -element V67() set
[:(Seg x),{y}:] is Relation-like complex-valued set
bool [:(Seg x),{y}:] is set
z is complex set
x |-> z is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
(Seg x) --> z is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{z}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{z}:]
{z} is non empty trivial 1 -element V67() set
[:(Seg x),{z}:] is Relation-like complex-valued set
bool [:(Seg x),{z}:] is set
((x |-> y),(x |-> z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((x |-> y),(x |-> z)) is Relation-like Function-like set
y + z is complex Element of COMPLEX
x |-> (y + z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
(Seg x) --> (y + z) is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{(y + z)}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{(y + z)}:]
{(y + z)} is non empty trivial 1 -element V67() set
[:(Seg x),{(y + z)}:] is Relation-like complex-valued set
bool [:(Seg x),{(y + z)}:] is set
x2 is complex Element of COMPLEX
x |-> x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> x2 is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{x2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{x2}:]
{x2} is non empty trivial 1 -element V67() set
[:(Seg x),{x2}:] is Relation-like complex-valued set
bool [:(Seg x),{x2}:] is set
y2 is complex Element of COMPLEX
x |-> y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> y2 is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{y2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{y2}:]
{y2} is non empty trivial 1 -element V67() set
[:(Seg x),{y2}:] is Relation-like complex-valued set
bool [:(Seg x),{y2}:] is set
(x,(x |-> x2),(x |-> y2)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex .: ((x |-> x2),(x |-> y2)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((x |-> x2),(x |-> y2)) is Relation-like Function-like set
addcomplex . (x2,y2) is complex Element of COMPLEX
[x2,y2] is set
{x2,y2} is V67() set
{{x2,y2},{x2}} is set
addcomplex . [x2,y2] is complex set
x |-> (addcomplex . (x2,y2)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> (addcomplex . (x2,y2)) is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{(addcomplex . (x2,y2))}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{(addcomplex . (x2,y2))}:]
{(addcomplex . (x2,y2))} is non empty trivial 1 -element V67() set
[:(Seg x),{(addcomplex . (x2,y2))}:] is Relation-like complex-valued set
bool [:(Seg x),{(addcomplex . (x2,y2))}:] is set
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
- x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
- 1 is complex real V38() set
(- 1) (#) x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
dom (- x) is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom x is V67() V68() V69() V70() V71() V72() Element of bool NAT
(x) is V67() Element of bool COMPLEX
dom compcomplex is non empty set
dom (x (#) compcomplex) is V67() V68() V69() V70() V71() V72() Element of bool NAT
z is set
dom y is V67() V68() V69() V70() V71() V72() Element of bool NAT
y . z is complex set
x . z is complex set
- (x . z) is complex Element of COMPLEX
compcomplex . (x . z) is complex set
(x (#) compcomplex) . z is complex set
z is set
dom y is V67() V68() V69() V70() V71() V72() Element of bool NAT
(- x) . z is complex set
x . z is complex set
- (x . z) is complex Element of COMPLEX
compcomplex . (x . z) is complex set
(x (#) compcomplex) . z is complex set
x is ordinal natural complex real V38() V45() cardinal set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
- y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] ((- 1),(id COMPLEX)) is Relation-like Function-like set
((- 1) multcomplex) * y is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * y is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
y (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
x is complex set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,x] is set
{1,x} is V67() set
{1} is non empty trivial 1 -element V67() V68() V69() V70() V71() V72() set
{{1,x},{1}} is set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*x*>) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(- 1) (#) <*x*> is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
<*x*> (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
- x is complex Element of COMPLEX
<*(- x)*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,(- x)] is set
{1,(- x)} is V67() set
{{1,(- x)},{1}} is set
{[1,(- x)]} is Relation-like Function-like constant non empty trivial 1 -element set
y is complex Element of COMPLEX
<*y*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,y] is set
{1,y} is V67() set
{{1,y},{1}} is set
{[1,y]} is Relation-like Function-like constant non empty trivial 1 -element set
(1,<*y*>) is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued Element of 1 -tuples_on COMPLEX
1 -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = 1 } is set
(- 1) (#) <*y*> is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * <*y*> is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * <*y*> is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
<*y*> (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
compcomplex . y is complex Element of COMPLEX
<*(compcomplex . y)*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,(compcomplex . y)] is set
{1,(compcomplex . y)} is V67() set
{{1,(compcomplex . y)},{1}} is set
{[1,(compcomplex . y)]} is Relation-like Function-like constant non empty trivial 1 -element set
x is ordinal natural complex real V38() V45() cardinal set
y is complex set
x |-> y is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> y is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{y}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{y}:]
{y} is non empty trivial 1 -element V67() set
[:(Seg x),{y}:] is Relation-like complex-valued set
bool [:(Seg x),{y}:] is set
((x |-> y)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(- 1) (#) (x |-> y) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(x |-> y) (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
- y is complex Element of COMPLEX
x |-> (- y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
(Seg x) --> (- y) is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{(- y)}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{(- y)}:]
{(- y)} is non empty trivial 1 -element V67() set
[:(Seg x),{(- y)}:] is Relation-like complex-valued set
bool [:(Seg x),{(- y)}:] is set
z is complex Element of COMPLEX
x |-> z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> z is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{z}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{z}:]
{z} is non empty trivial 1 -element V67() set
[:(Seg x),{z}:] is Relation-like complex-valued set
bool [:(Seg x),{z}:] is set
(x,(x |-> z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(- 1) (#) (x |-> z) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * (x |-> z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * (x |-> z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x |-> z) (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
compcomplex . z is complex Element of COMPLEX
x |-> (compcomplex . z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> (compcomplex . z) is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{(compcomplex . z)}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{(compcomplex . z)}:]
{(compcomplex . z)} is non empty trivial 1 -element V67() set
[:(Seg x),{(compcomplex . z)}:] is Relation-like complex-valued set
bool [:(Seg x),{(compcomplex . z)}:] is set
x is ordinal natural complex real V38() V45() cardinal set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
addcomplex .: (y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (y,z) is Relation-like Function-like set
x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,x2,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex .: (x2,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (x2,z) is Relation-like Function-like set
(x,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(- 1) (#) z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(x,z,(x,z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex .: (z,(x,z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (z,(x,z)) is Relation-like Function-like set
(x,y,(x,z,(x,z))) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex .: (y,(x,z,(x,z))) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (y,(x,z,(x,z))) is Relation-like Function-like set
(x,(x,x2,z),(x,z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex .: ((x,x2,z),(x,z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((x,x2,z),(x,z)) is Relation-like Function-like set
(x,x2,(x,z,(x,z))) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex .: (x2,(x,z,(x,z))) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (x2,(x,z,(x,z))) is Relation-like Function-like set
0c is complex Element of COMPLEX
x |-> 0c is Relation-like empty-yielding NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of x -tuples_on COMPLEX
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> 0c is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{0c}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{0c}:]
{0c} is non empty trivial 1 -element V67() set
[:(Seg x),{0c}:] is Relation-like complex-valued set
bool [:(Seg x),{0c}:] is set
(x,x2,(x |-> 0c)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex .: (x2,(x |-> 0c)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (x2,(x |-> 0c)) is Relation-like Function-like set
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(x) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(- 1) (#) x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(x,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (x,y) is Relation-like Function-like set
((x,y)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(- 1) (#) (x,y) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * (x,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * (x,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,y) (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(- 1) (#) y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((x),(y)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((x),(y)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((x),(y)) is Relation-like Function-like set
dom ((x,y)) is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom (x,y) is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom x is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom y is V67() V68() V69() V70() V71() V72() Element of bool NAT
(dom x) /\ (dom y) is V67() V68() V69() V70() V71() V72() set
dom ((x),(y)) is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom (x) is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom (y) is V67() V68() V69() V70() V71() V72() Element of bool NAT
(dom (x)) /\ (dom (y)) is V67() V68() V69() V70() V71() V72() set
(dom x) /\ (dom (y)) is V67() V68() V69() V70() V71() V72() set
z is ordinal natural complex real V38() V45() cardinal set
((x,y)) . z is complex set
(x,y) . z is complex set
- ((x,y) . z) is complex Element of COMPLEX
x . z is complex set
y . z is complex set
(x . z) + (y . z) is complex Element of COMPLEX
- ((x . z) + (y . z)) is complex Element of COMPLEX
- (x . z) is complex Element of COMPLEX
- (y . z) is complex Element of COMPLEX
(- (x . z)) + (- (y . z)) is complex Element of COMPLEX
(y) . z is complex set
(- (x . z)) + ((y) . z) is complex Element of COMPLEX
(x) . z is complex set
((x) . z) + ((y) . z) is complex Element of COMPLEX
((x),(y)) . z is complex set
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x - y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
- y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x + (- y) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (x,(- y)) is Relation-like Function-like set
diffcomplex .: (x,y) is Relation-like Function-like set
y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
dom (x - y) is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom x is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom y is V67() V68() V69() V70() V71() V72() Element of bool NAT
(dom x) /\ (dom y) is V67() V68() V69() V70() V71() V72() set
dom diffcomplex is set
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(z) is V67() Element of bool COMPLEX
x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x2) is V67() Element of bool COMPLEX
[:(z),(x2):] is Relation-like complex-valued set
dom (diffcomplex .: (x,y)) is set
z2 is set
y2 . z2 is complex set
x . z2 is complex set
y . z2 is complex set
diffcomplex . ((x . z2),(y . z2)) is set
[(x . z2),(y . z2)] is set
{(x . z2),(y . z2)} is V67() set
{(x . z2)} is non empty trivial 1 -element V67() set
{{(x . z2),(y . z2)},{(x . z2)}} is set
diffcomplex . [(x . z2),(y . z2)] is complex set
(x . z2) - (y . z2) is complex Element of COMPLEX
- (y . z2) is complex set
(x . z2) + (- (y . z2)) is set
z2 is set
dom y2 is V67() V68() V69() V70() V71() V72() Element of bool NAT
y2 . z2 is complex set
x . z2 is complex set
y . z2 is complex set
diffcomplex . ((x . z2),(y . z2)) is set
[(x . z2),(y . z2)] is set
{(x . z2),(y . z2)} is V67() set
{(x . z2)} is non empty trivial 1 -element V67() set
{{(x . z2),(y . z2)},{(x . z2)}} is set
diffcomplex . [(x . z2),(y . z2)] is complex set
(x . z2) - (y . z2) is complex Element of COMPLEX
- (y . z2) is complex set
(x . z2) + (- (y . z2)) is set
x is ordinal natural complex real V38() V45() cardinal set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
y - z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
- z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y + (- z) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (y,(- z)) is Relation-like Function-like set
diffcomplex .: (y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
diffcomplex .: (y,z) is Relation-like Function-like set
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
x is set
y is ordinal natural complex real V38() V45() cardinal set
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() y -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z . x is complex set
x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() y -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(y,z,x2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() y -element FinSequence-like FinSubsequence-like complex-valued Element of y -tuples_on COMPLEX
y -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = y } is set
- x2 is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) x2 is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
x2 (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
z + (- x2) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (z,(- x2)) is Relation-like Function-like set
diffcomplex .: (z,x2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
diffcomplex .: (z,x2) is Relation-like Function-like set
(y,z,x2) . x is complex set
x2 . x is complex set
(z . x) - (x2 . x) is complex Element of COMPLEX
- (x2 . x) is complex set
(z . x) + (- (x2 . x)) is set
Seg y is V45() y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,y) ) } is set
dom x2 is y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
dom z is y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
dom (y,z,x2) is y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
0 - 0 is complex real V38() V41() V42() Element of INT
- 0 is complex real V38() set
0 + (- 0) is complex real V38() set
(z . x) - 0 is complex Element of COMPLEX
(z . x) + (- 0) is set
Seg y is V45() y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,y) ) } is set
dom (y,z,x2) is y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
Seg y is V45() y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,y) ) } is set
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((<*> COMPLEX),x) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
- x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(<*> COMPLEX) + (- x) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: ((<*> COMPLEX),(- x)) is Relation-like Function-like set
diffcomplex .: ((<*> COMPLEX),x) is Relation-like Function-like set
(x,(<*> COMPLEX)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
- (<*> COMPLEX) is Relation-like NAT -defined RAT -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(- 1) (#) (<*> COMPLEX) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(- 1) multreal 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 is Relation-like Function-like V14([:REAL,REAL:]) V18([:REAL,REAL:], REAL ) commutative associative V37( REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
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 V61() non-decreasing Element of bool [:REAL,REAL:]
multreal [;] ((- 1),(id REAL)) is Relation-like Function-like set
(<*> COMPLEX) (#) ((- 1) multreal) is Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ordinal natural complex real V38() Function-yielding V44() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V67() V68() V69() V70() V71() V72() V73() set
((- 1) multcomplex) * (<*> COMPLEX) is Relation-like non-zero empty-yielding NAT -defined COMPLEX -valued RAT -valued Function-like one-to-one constant functional empty ordinal natural complex real V38() Function-yielding V44() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V67() V68() V69() V70() V71() V72() V73() FinSequence of 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:]
(<*> COMPLEX) (#) compreal is Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ordinal natural complex real V38() Function-yielding V44() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V67() V68() V69() V70() V71() V72() V73() set
compcomplex * (<*> COMPLEX) is Relation-like non-zero empty-yielding NAT -defined COMPLEX -valued RAT -valued Function-like one-to-one constant functional empty ordinal natural complex real V38() Function-yielding V44() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V67() V68() V69() V70() V71() V72() V73() FinSequence of COMPLEX
(<*> COMPLEX) (#) compcomplex is Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ordinal natural complex real V38() Function-yielding V44() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V67() V68() V69() V70() V71() V72() V73() set
x + (- (<*> COMPLEX)) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (x,(- (<*> COMPLEX))) is Relation-like Function-like set
diffcomplex .: (x,(<*> COMPLEX)) is Relation-like Function-like set
x is complex set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,x] is set
{1,x} is V67() set
{1} is non empty trivial 1 -element V67() V68() V69() V70() V71() V72() set
{{1,x},{1}} is set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
y is complex set
<*y*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,y] is set
{1,y} is V67() set
{{1,y},{1}} is set
{[1,y]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*x*>,<*y*>) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
- <*y*> is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) <*y*> is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
<*y*> (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
<*x*> + (- <*y*>) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (<*x*>,(- <*y*>)) is Relation-like Function-like set
diffcomplex .: (<*x*>,<*y*>) is Relation-like Function-like set
x - y is complex Element of COMPLEX
- y is complex set
x + (- y) is set
<*(x - y)*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,(x - y)] is set
{1,(x - y)} is V67() set
{{1,(x - y)},{1}} is set
{[1,(x - y)]} is Relation-like Function-like constant non empty trivial 1 -element set
z is complex Element of COMPLEX
<*z*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,z] is set
{1,z} is V67() set
{{1,z},{1}} is set
{[1,z]} is Relation-like Function-like constant non empty trivial 1 -element set
x2 is complex Element of COMPLEX
<*x2*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,x2] is set
{1,x2} is V67() set
{{1,x2},{1}} is set
{[1,x2]} is Relation-like Function-like constant non empty trivial 1 -element set
(1,<*z*>,<*x2*>) is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued Element of 1 -tuples_on COMPLEX
1 -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = 1 } is set
- <*x2*> is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) <*x2*> is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * <*x2*> is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * <*x2*> is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
<*x2*> (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
<*z*> + (- <*x2*>) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (<*z*>,(- <*x2*>)) is Relation-like Function-like set
diffcomplex .: (<*z*>,<*x2*>) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
diffcomplex .: (<*z*>,<*x2*>) is Relation-like Function-like set
diffcomplex . (z,x2) is complex Element of COMPLEX
[z,x2] is set
{z,x2} is V67() set
{z} is non empty trivial 1 -element V67() set
{{z,x2},{z}} is set
diffcomplex . [z,x2] is complex set
<*(diffcomplex . (z,x2))*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,(diffcomplex . (z,x2))] is set
{1,(diffcomplex . (z,x2))} is V67() set
{{1,(diffcomplex . (z,x2))},{1}} is set
{[1,(diffcomplex . (z,x2))]} is Relation-like Function-like constant non empty trivial 1 -element set
x is ordinal natural complex real V38() V45() cardinal set
y is complex set
x |-> y is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> y is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{y}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{y}:]
{y} is non empty trivial 1 -element V67() set
[:(Seg x),{y}:] is Relation-like complex-valued set
bool [:(Seg x),{y}:] is set
z is complex set
x |-> z is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
(Seg x) --> z is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{z}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{z}:]
{z} is non empty trivial 1 -element V67() set
[:(Seg x),{z}:] is Relation-like complex-valued set
bool [:(Seg x),{z}:] is set
((x |-> y),(x |-> z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
- (x |-> z) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) (x |-> z) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(x |-> z) (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(x |-> y) + (- (x |-> z)) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: ((x |-> y),(- (x |-> z))) is Relation-like Function-like set
diffcomplex .: ((x |-> y),(x |-> z)) is Relation-like Function-like set
y - z is complex Element of COMPLEX
- z is complex set
y + (- z) is set
x |-> (y - z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
(Seg x) --> (y - z) is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{(y - z)}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{(y - z)}:]
{(y - z)} is non empty trivial 1 -element V67() set
[:(Seg x),{(y - z)}:] is Relation-like complex-valued set
bool [:(Seg x),{(y - z)}:] is set
x2 is complex Element of COMPLEX
x |-> x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> x2 is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{x2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{x2}:]
{x2} is non empty trivial 1 -element V67() set
[:(Seg x),{x2}:] is Relation-like complex-valued set
bool [:(Seg x),{x2}:] is set
y2 is complex Element of COMPLEX
x |-> y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> y2 is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{y2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{y2}:]
{y2} is non empty trivial 1 -element V67() set
[:(Seg x),{y2}:] is Relation-like complex-valued set
bool [:(Seg x),{y2}:] is set
(x,(x |-> x2),(x |-> y2)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
- (x |-> y2) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) (x |-> y2) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * (x |-> y2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * (x |-> y2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x |-> y2) (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(x |-> x2) + (- (x |-> y2)) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: ((x |-> x2),(- (x |-> y2))) is Relation-like Function-like set
diffcomplex .: ((x |-> x2),(x |-> y2)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
diffcomplex .: ((x |-> x2),(x |-> y2)) is Relation-like Function-like set
diffcomplex . (x2,y2) is complex Element of COMPLEX
[x2,y2] is set
{x2,y2} is V67() set
{{x2,y2},{x2}} is set
diffcomplex . [x2,y2] is complex set
x |-> (diffcomplex . (x2,y2)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> (diffcomplex . (x2,y2)) is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{(diffcomplex . (x2,y2))}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{(diffcomplex . (x2,y2))}:]
{(diffcomplex . (x2,y2))} is non empty trivial 1 -element V67() set
[:(Seg x),{(diffcomplex . (x2,y2))}:] is Relation-like complex-valued set
bool [:(Seg x),{(diffcomplex . (x2,y2))}:] is set
0c is complex Element of COMPLEX
x is ordinal natural complex real V38() V45() cardinal set
x |-> 0c is Relation-like empty-yielding NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> 0c is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{0c}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{0c}:]
{0c} is non empty trivial 1 -element V67() set
[:(Seg x),{0c}:] is Relation-like complex-valued set
bool [:(Seg x),{0c}:] is set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,y,(x |-> 0c)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
- (x |-> 0c) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(- 1) (#) (x |-> 0c) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(- 1) multreal 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 is Relation-like Function-like V14([:REAL,REAL:]) V18([:REAL,REAL:], REAL ) commutative associative V37( REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
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 V61() non-decreasing Element of bool [:REAL,REAL:]
multreal [;] ((- 1),(id REAL)) is Relation-like Function-like set
(x |-> 0c) (#) ((- 1) multreal) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
((- 1) multcomplex) * (x |-> 0c) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of 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:]
(x |-> 0c) (#) compreal is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
compcomplex * (x |-> 0c) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x |-> 0c) (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y + (- (x |-> 0c)) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (y,(- (x |-> 0c))) is Relation-like Function-like set
diffcomplex .: (y,(x |-> 0c)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
diffcomplex .: (y,(x |-> 0c)) is Relation-like Function-like set
- 0 is complex real V38() V41() V42() Element of INT
x |-> (- 0) is Relation-like NAT -defined INT -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of x -tuples_on INT
x -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
INT * is functional non empty FinSequence-membered FinSequenceSet of INT
{ b1 where b1 is Relation-like NAT -defined INT -valued Function-like V45() FinSequence-like FinSubsequence-like Element of INT * : len b1 = x } is set
(Seg x) --> (- 0) is Relation-like Seg x -defined Seg x -defined RAT -valued INT -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{(- 0)}) V45() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of bool [:(Seg x),{(- 0)}:]
{(- 0)} is non empty trivial 1 -element V67() V68() V69() V70() V71() set
[:(Seg x),{(- 0)}:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
bool [:(Seg x),{(- 0)}:] is set
(y,(x |-> (- 0))) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (y,(x |-> (- 0))) is Relation-like Function-like set
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(x,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
- y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x + (- y) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (x,(- y)) is Relation-like Function-like set
diffcomplex .: (x,y) is Relation-like Function-like set
((x,y)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(- 1) (#) (x,y) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * (x,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * (x,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,y) (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(y,x) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
- x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y + (- x) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (y,(- x)) is Relation-like Function-like set
diffcomplex .: (y,x) is Relation-like Function-like set
(x) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
((y)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(- 1) (#) (y) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * (y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * (y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(y) (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((x),((y))) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((x),((y))) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((x),((y))) is Relation-like Function-like set
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(x) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(- 1) (#) x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(x,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
- y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x + (- y) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (x,(- y)) is Relation-like Function-like set
diffcomplex .: (x,y) is Relation-like Function-like set
((x,y)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(- 1) (#) (x,y) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * (x,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * (x,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,y) (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((x),y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((x),y) is Relation-like Function-like set
(y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
((y)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(- 1) (#) (y) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * (y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * (y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(y) (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((x),((y))) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((x),((y))) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((x),((y))) is Relation-like Function-like set
x is ordinal natural complex real V38() V45() cardinal set
x |-> 0c is Relation-like empty-yielding NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> 0c is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{0c}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{0c}:]
{0c} is non empty trivial 1 -element V67() set
[:(Seg x),{0c}:] is Relation-like complex-valued set
bool [:(Seg x),{0c}:] is set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
- z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y + (- z) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (y,(- z)) is Relation-like Function-like set
diffcomplex .: (y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
diffcomplex .: (y,z) is Relation-like Function-like set
(x,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(x,(x,z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(- 1) (#) (x,z) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * (x,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * (x,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,z) (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x is ordinal natural complex real V38() V45() cardinal set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
addcomplex .: (y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (y,z) is Relation-like Function-like set
(x,(x,y,z),z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
- z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(x,y,z) + (- z) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: ((x,y,z),(- z)) is Relation-like Function-like set
diffcomplex .: ((x,y,z),z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
diffcomplex .: ((x,y,z),z) is Relation-like Function-like set
x |-> 0c is Relation-like empty-yielding NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of x -tuples_on COMPLEX
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> 0c is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{0c}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{0c}:]
{0c} is non empty trivial 1 -element V67() set
[:(Seg x),{0c}:] is Relation-like complex-valued set
bool [:(Seg x),{0c}:] is set
(x,y,(x |-> 0c)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex .: (y,(x |-> 0c)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (y,(x |-> 0c)) is Relation-like Function-like set
(x,z,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
z + (- z) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (z,(- z)) is Relation-like Function-like set
diffcomplex .: (z,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
diffcomplex .: (z,z) is Relation-like Function-like set
(x,y,(x,z,z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex .: (y,(x,z,z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (y,(x,z,z)) is Relation-like Function-like set
x is ordinal natural complex real V38() V45() cardinal set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
- z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
compcomplex * z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y + (- z) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (y,(- z)) is Relation-like Function-like set
diffcomplex .: (y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
diffcomplex .: (y,z) is Relation-like Function-like set
(x,(x,y,z),z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex .: ((x,y,z),z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((x,y,z),z) is Relation-like Function-like set
x |-> 0c is Relation-like empty-yielding NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of x -tuples_on COMPLEX
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> 0c is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{0c}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{0c}:]
{0c} is non empty trivial 1 -element V67() set
[:(Seg x),{0c}:] is Relation-like complex-valued set
bool [:(Seg x),{0c}:] is set
(x,y,(x |-> 0c)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex .: (y,(x |-> 0c)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (y,(x |-> 0c)) is Relation-like Function-like set
(x,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(x,(x,z),z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex .: ((x,z),z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((x,z),z) is Relation-like Function-like set
(x,y,(x,(x,z),z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex .: (y,(x,(x,z),z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (y,(x,(x,z),z)) is Relation-like Function-like set
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y is complex set
y (#) x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (y,(id COMPLEX)) is Relation-like Function-like set
x (#) (y multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
dom (y (#) x) is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom x is V67() V68() V69() V70() V71() V72() Element of bool NAT
(x) is V67() Element of bool COMPLEX
dom (y multcomplex) is non empty set
dom (x (#) (y multcomplex)) is V67() V68() V69() V70() V71() V72() Element of bool NAT
x2 is set
dom z is V67() V68() V69() V70() V71() V72() Element of bool NAT
z . x2 is complex set
x . x2 is complex set
y * (x . x2) is complex Element of COMPLEX
(y multcomplex) . (x . x2) is complex set
(x (#) (y multcomplex)) . x2 is complex set
x2 is set
dom z is V67() V68() V69() V70() V71() V72() Element of bool NAT
(y (#) x) . x2 is complex set
x . x2 is complex set
y * (x . x2) is complex Element of COMPLEX
(y multcomplex) . (x . x2) is complex set
(x (#) (y multcomplex)) . x2 is complex set
x is ordinal natural complex real V38() V45() cardinal set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z is complex set
z (#) y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
z multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (z,(id COMPLEX)) is Relation-like Function-like set
(z multcomplex) * y is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
y (#) (z multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
x is complex set
y is complex set
<*y*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,y] is set
{1,y} is V67() set
{1} is non empty trivial 1 -element V67() V68() V69() V70() V71() V72() set
{{1,y},{1}} is set
{[1,y]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*y*>,x) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
x multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (x,(id COMPLEX)) is Relation-like Function-like set
<*y*> (#) (x multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x * y is complex Element of COMPLEX
<*(x * y)*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,(x * y)] is set
{1,(x * y)} is V67() set
{{1,(x * y)},{1}} is set
{[1,(x * y)]} is Relation-like Function-like constant non empty trivial 1 -element set
x2 is complex Element of COMPLEX
<*x2*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,x2] is set
{1,x2} is V67() set
{{1,x2},{1}} is set
{[1,x2]} is Relation-like Function-like constant non empty trivial 1 -element set
z is complex Element of COMPLEX
(1,<*x2*>,z) is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued Element of 1 -tuples_on COMPLEX
1 -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = 1 } is set
z multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (z,(id COMPLEX)) is Relation-like Function-like set
(z multcomplex) * <*x2*> is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
<*x2*> (#) (z multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
multcomplex [;] (z,(id COMPLEX)) is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
(multcomplex [;] (z,(id COMPLEX))) . x2 is complex Element of COMPLEX
<*((multcomplex [;] (z,(id COMPLEX))) . x2)*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,((multcomplex [;] (z,(id COMPLEX))) . x2)] is set
{1,((multcomplex [;] (z,(id COMPLEX))) . x2)} is V67() set
{{1,((multcomplex [;] (z,(id COMPLEX))) . x2)},{1}} is set
{[1,((multcomplex [;] (z,(id COMPLEX))) . x2)]} is Relation-like Function-like constant non empty trivial 1 -element set
x is ordinal natural complex real V38() V45() cardinal set
y is complex set
z is complex set
x |-> z is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> z is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{z}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{z}:]
{z} is non empty trivial 1 -element V67() set
[:(Seg x),{z}:] is Relation-like complex-valued set
bool [:(Seg x),{z}:] is set
((x |-> z),y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
y multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (y,(id COMPLEX)) is Relation-like Function-like set
(x |-> z) (#) (y multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y * z is complex Element of COMPLEX
x |-> (y * z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
(Seg x) --> (y * z) is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{(y * z)}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{(y * z)}:]
{(y * z)} is non empty trivial 1 -element V67() set
[:(Seg x),{(y * z)}:] is Relation-like complex-valued set
bool [:(Seg x),{(y * z)}:] is set
y2 is complex Element of COMPLEX
x |-> y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> y2 is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{y2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{y2}:]
{y2} is non empty trivial 1 -element V67() set
[:(Seg x),{y2}:] is Relation-like complex-valued set
bool [:(Seg x),{y2}:] is set
x2 is complex Element of COMPLEX
(x,(x |-> y2),x2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x2 multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (x2,(id COMPLEX)) is Relation-like Function-like set
(x2 multcomplex) * (x |-> y2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x |-> y2) (#) (x2 multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
multcomplex [;] (x2,(id COMPLEX)) is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
(multcomplex [;] (x2,(id COMPLEX))) . y2 is complex Element of COMPLEX
x |-> ((multcomplex [;] (x2,(id COMPLEX))) . y2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> ((multcomplex [;] (x2,(id COMPLEX))) . y2) is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{((multcomplex [;] (x2,(id COMPLEX))) . y2)}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{((multcomplex [;] (x2,(id COMPLEX))) . y2)}:]
{((multcomplex [;] (x2,(id COMPLEX))) . y2)} is non empty trivial 1 -element V67() set
[:(Seg x),{((multcomplex [;] (x2,(id COMPLEX))) . y2)}:] is Relation-like complex-valued set
bool [:(Seg x),{((multcomplex [;] (x2,(id COMPLEX))) . y2)}:] is set
x is complex set
y is complex set
x + y is complex Element of COMPLEX
z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(z,(x + y)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x + y) multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] ((x + y),(id COMPLEX)) is Relation-like Function-like set
z (#) ((x + y) multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(z,x) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
x multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (x,(id COMPLEX)) is Relation-like Function-like set
z (#) (x multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(z,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
y multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (y,(id COMPLEX)) is Relation-like Function-like set
z (#) (y multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((z,x),(z,y)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((z,x),(z,y)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((z,x),(z,y)) is Relation-like Function-like set
dom (z,(x + y)) is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom z is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom ((z,x),(z,y)) is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom (z,x) is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom (z,y) is V67() V68() V69() V70() V71() V72() Element of bool NAT
(dom (z,x)) /\ (dom (z,y)) is V67() V68() V69() V70() V71() V72() set
x2 is ordinal natural complex real V38() V45() cardinal set
(z,(x + y)) . x2 is complex set
z . x2 is complex set
(x + y) * (z . x2) is complex Element of COMPLEX
x * (z . x2) is complex Element of COMPLEX
y * (z . x2) is complex Element of COMPLEX
(x * (z . x2)) + (y * (z . x2)) is complex Element of COMPLEX
(z,y) . x2 is complex set
(x * (z . x2)) + ((z,y) . x2) is complex Element of COMPLEX
(z,x) . x2 is complex set
((z,x) . x2) + ((z,y) . x2) is complex Element of COMPLEX
((z,x),(z,y)) . x2 is complex set
x is ordinal natural complex real V38() V45() cardinal set
x |-> 0c is Relation-like empty-yielding NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> 0c is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{0c}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{0c}:]
{0c} is non empty trivial 1 -element V67() set
[:(Seg x),{0c}:] is Relation-like complex-valued set
bool [:(Seg x),{0c}:] is set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,y,0c) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
0c multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (0c,(id COMPLEX)) is Relation-like Function-like set
(0c multcomplex) * y is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
y (#) (0c multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(y) is V67() Element of bool COMPLEX
(id COMPLEX) * y is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
multcomplex [;] (0c,((id COMPLEX) * y)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
multcomplex [;] (0c,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x (#) y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
multcomplex .: (x,y) is Relation-like Function-like set
y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
dom multcomplex is set
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(z) is V67() Element of bool COMPLEX
x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x2) is V67() Element of bool COMPLEX
[:(z),(x2):] is Relation-like complex-valued set
dom (multcomplex .: (x,y)) is set
dom x is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom y is V67() V68() V69() V70() V71() V72() Element of bool NAT
(dom x) /\ (dom y) is V67() V68() V69() V70() V71() V72() set
dom (x (#) y) is V67() V68() V69() V70() V71() V72() Element of bool NAT
z2 is set
y2 . z2 is complex set
x . z2 is complex set
y . z2 is complex set
multcomplex . ((x . z2),(y . z2)) is set
[(x . z2),(y . z2)] is set
{(x . z2),(y . z2)} is V67() set
{(x . z2)} is non empty trivial 1 -element V67() set
{{(x . z2),(y . z2)},{(x . z2)}} is set
multcomplex . [(x . z2),(y . z2)] is complex set
(x . z2) * (y . z2) is complex Element of COMPLEX
z2 is set
dom y2 is V67() V68() V69() V70() V71() V72() Element of bool NAT
y2 . z2 is complex set
x . z2 is complex set
y . z2 is complex set
multcomplex . ((x . z2),(y . z2)) is set
[(x . z2),(y . z2)] is set
{(x . z2),(y . z2)} is V67() set
{(x . z2)} is non empty trivial 1 -element V67() set
{{(x . z2),(y . z2)},{(x . z2)}} is set
multcomplex . [(x . z2),(y . z2)] is complex set
(x . z2) * (y . z2) is complex Element of COMPLEX
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
x2 is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y2 is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
multcomplex .: (x2,y2) is Relation-like Function-like set
multcomplex .: (y2,x2) is Relation-like Function-like set
dom multcomplex is set
i is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(i) is V67() Element of bool COMPLEX
z2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(z2) is V67() Element of bool COMPLEX
[:(i),(z2):] is Relation-like complex-valued set
[:(z2),(i):] is Relation-like complex-valued set
dom (multcomplex .: (x2,y2)) is set
dom x2 is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom y2 is V67() V68() V69() V70() V71() V72() Element of bool NAT
(dom x2) /\ (dom y2) is V67() V68() V69() V70() V71() V72() set
dom (multcomplex .: (y2,x2)) is set
a is set
z . a is complex set
y2 . a is complex set
x2 . a is complex set
multcomplex . ((y2 . a),(x2 . a)) is set
[(y2 . a),(x2 . a)] is set
{(y2 . a),(x2 . a)} is V67() set
{(y2 . a)} is non empty trivial 1 -element V67() set
{{(y2 . a),(x2 . a)},{(y2 . a)}} is set
multcomplex . [(y2 . a),(x2 . a)] is complex set
multcomplex . ((x2 . a),(y2 . a)) is set
[(x2 . a),(y2 . a)] is set
{(x2 . a),(y2 . a)} is V67() set
{(x2 . a)} is non empty trivial 1 -element V67() set
{{(x2 . a),(y2 . a)},{(x2 . a)}} is set
multcomplex . [(x2 . a),(y2 . a)] is complex set
(x2 . a) * (y2 . a) is complex Element of COMPLEX
x is ordinal natural complex real V38() V45() cardinal set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
y (#) z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
multcomplex .: (y,z) is Relation-like Function-like set
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((<*> COMPLEX),x) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
multcomplex .: ((<*> COMPLEX),x) is Relation-like Function-like set
x is complex set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,x] is set
{1,x} is V67() set
{1} is non empty trivial 1 -element V67() V68() V69() V70() V71() V72() set
{{1,x},{1}} is set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
y is complex set
<*y*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,y] is set
{1,y} is V67() set
{{1,y},{1}} is set
{[1,y]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*x*>,<*y*>) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
multcomplex .: (<*x*>,<*y*>) is Relation-like Function-like set
x * y is complex Element of COMPLEX
<*(x * y)*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,(x * y)] is set
{1,(x * y)} is V67() set
{{1,(x * y)},{1}} is set
{[1,(x * y)]} is Relation-like Function-like constant non empty trivial 1 -element set
z is complex Element of COMPLEX
<*z*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,z] is set
{1,z} is V67() set
{{1,z},{1}} is set
{[1,z]} is Relation-like Function-like constant non empty trivial 1 -element set
x2 is complex Element of COMPLEX
<*x2*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,x2] is set
{1,x2} is V67() set
{{1,x2},{1}} is set
{[1,x2]} is Relation-like Function-like constant non empty trivial 1 -element set
(1,<*z*>,<*x2*>) is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued Element of 1 -tuples_on COMPLEX
1 -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = 1 } is set
multcomplex .: (<*z*>,<*x2*>) is Relation-like Function-like set
multcomplex . (z,x2) is complex Element of COMPLEX
[z,x2] is set
{z,x2} is V67() set
{z} is non empty trivial 1 -element V67() set
{{z,x2},{z}} is set
multcomplex . [z,x2] is complex set
<*(multcomplex . (z,x2))*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,(multcomplex . (z,x2))] is set
{1,(multcomplex . (z,x2))} is V67() set
{{1,(multcomplex . (z,x2))},{1}} is set
{[1,(multcomplex . (z,x2))]} is Relation-like Function-like constant non empty trivial 1 -element set
x is ordinal natural complex real V38() V45() cardinal set
y is complex set
x |-> y is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> y is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{y}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{y}:]
{y} is non empty trivial 1 -element V67() set
[:(Seg x),{y}:] is Relation-like complex-valued set
bool [:(Seg x),{y}:] is set
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
((x |-> y),z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
multcomplex .: ((x |-> y),z) is Relation-like Function-like set
(x,z,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
y multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (y,(id COMPLEX)) is Relation-like Function-like set
(y multcomplex) * z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z (#) (y multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x2 is complex Element of COMPLEX
x |-> x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> x2 is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{x2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{x2}:]
{x2} is non empty trivial 1 -element V67() set
[:(Seg x),{x2}:] is Relation-like complex-valued set
bool [:(Seg x),{x2}:] is set
(x,(x |-> x2),z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
multcomplex .: ((x |-> x2),z) is Relation-like Function-like set
multcomplex [;] (x2,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
x is ordinal natural complex real V38() V45() cardinal set
y is complex set
x |-> y is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> y is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{y}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{y}:]
{y} is non empty trivial 1 -element V67() set
[:(Seg x),{y}:] is Relation-like complex-valued set
bool [:(Seg x),{y}:] is set
z is complex set
x |-> z is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
(Seg x) --> z is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{z}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{z}:]
{z} is non empty trivial 1 -element V67() set
[:(Seg x),{z}:] is Relation-like complex-valued set
bool [:(Seg x),{z}:] is set
((x |-> y),(x |-> z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
multcomplex .: ((x |-> y),(x |-> z)) is Relation-like Function-like set
y * z is complex Element of COMPLEX
x |-> (y * z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
(Seg x) --> (y * z) is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{(y * z)}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{(y * z)}:]
{(y * z)} is non empty trivial 1 -element V67() set
[:(Seg x),{(y * z)}:] is Relation-like complex-valued set
bool [:(Seg x),{(y * z)}:] is set
x2 is complex Element of COMPLEX
x |-> x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> x2 is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{x2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{x2}:]
{x2} is non empty trivial 1 -element V67() set
[:(Seg x),{x2}:] is Relation-like complex-valued set
bool [:(Seg x),{x2}:] is set
y2 is complex Element of COMPLEX
x |-> y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> y2 is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{y2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{y2}:]
{y2} is non empty trivial 1 -element V67() set
[:(Seg x),{y2}:] is Relation-like complex-valued set
bool [:(Seg x),{y2}:] is set
(x,(x |-> x2),(x |-> y2)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
multcomplex .: ((x |-> x2),(x |-> y2)) is Relation-like Function-like set
(x,(x |-> y2),x2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x2 multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (x2,(id COMPLEX)) is Relation-like Function-like set
(x2 multcomplex) * (x |-> y2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x |-> y2) (#) (x2 multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
Sum (<*> COMPLEX) is complex real V38() Element of COMPLEX
addcomplex $$ (<*> COMPLEX) is complex Element of COMPLEX
x is complex set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,x] is set
{1,x} is V67() set
{1} is non empty trivial 1 -element V67() V68() V69() V70() V71() V72() set
{{1,x},{1}} is set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
Sum <*x*> is complex set
y is complex Element of COMPLEX
<*y*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,y] is set
{1,y} is V67() set
{{1,y},{1}} is set
{[1,y]} is Relation-like Function-like constant non empty trivial 1 -element set
Sum <*y*> is complex Element of COMPLEX
addcomplex $$ <*y*> is complex Element of COMPLEX
x is complex set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,x] is set
{1,x} is V67() set
{1} is non empty trivial 1 -element V67() V68() V69() V70() V71() V72() set
{{1,x},{1}} is set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y ^ <*x*> is Relation-like NAT -defined Function-like non empty V45() FinSequence-like FinSubsequence-like complex-valued set
Sum (y ^ <*x*>) is complex set
Sum y is complex set
(Sum y) + x is complex Element of COMPLEX
x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z is complex Element of COMPLEX
<*z*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,z] is set
{1,z} is V67() set
{{1,z},{1}} is set
{[1,z]} is Relation-like Function-like constant non empty trivial 1 -element set
x2 ^ <*z*> is Relation-like NAT -defined COMPLEX -valued Function-like non empty V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
Sum (x2 ^ <*z*>) is complex Element of COMPLEX
addcomplex $$ (x2 ^ <*z*>) is complex Element of COMPLEX
addcomplex $$ x2 is complex Element of COMPLEX
addcomplex . ((addcomplex $$ x2),z) is complex Element of COMPLEX
[(addcomplex $$ x2),z] is set
{(addcomplex $$ x2),z} is V67() set
{(addcomplex $$ x2)} is non empty trivial 1 -element V67() set
{{(addcomplex $$ x2),z},{(addcomplex $$ x2)}} is set
addcomplex . [(addcomplex $$ x2),z] is complex set
Sum x2 is complex Element of COMPLEX
(Sum x2) + x is complex Element of COMPLEX
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
Sum x is complex set
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x ^ y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
Sum (x ^ y) is complex set
Sum y is complex set
(Sum x) + (Sum y) is complex Element of COMPLEX
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z ^ x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
Sum (z ^ x2) is complex Element of COMPLEX
addcomplex $$ (z ^ x2) is complex Element of COMPLEX
addcomplex $$ z is complex Element of COMPLEX
addcomplex $$ x2 is complex Element of COMPLEX
addcomplex . ((addcomplex $$ z),(addcomplex $$ x2)) is complex Element of COMPLEX
[(addcomplex $$ z),(addcomplex $$ x2)] is set
{(addcomplex $$ z),(addcomplex $$ x2)} is V67() set
{(addcomplex $$ z)} is non empty trivial 1 -element V67() set
{{(addcomplex $$ z),(addcomplex $$ x2)},{(addcomplex $$ z)}} is set
addcomplex . [(addcomplex $$ z),(addcomplex $$ x2)] is complex set
Sum z is complex Element of COMPLEX
Sum x2 is complex Element of COMPLEX
(Sum z) + (Sum x2) is complex Element of COMPLEX
x is complex set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,x] is set
{1,x} is V67() set
{1} is non empty trivial 1 -element V67() V68() V69() V70() V71() V72() set
{{1,x},{1}} is set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
<*x*> ^ y is Relation-like NAT -defined Function-like non empty V45() FinSequence-like FinSubsequence-like complex-valued set
Sum (<*x*> ^ y) is complex set
Sum y is complex set
x + (Sum y) is complex Element of COMPLEX
z is complex Element of COMPLEX
<*z*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,z] is set
{1,z} is V67() set
{{1,z},{1}} is set
{[1,z]} is Relation-like Function-like constant non empty trivial 1 -element set
Sum <*z*> is complex Element of COMPLEX
addcomplex $$ <*z*> is complex Element of COMPLEX
(Sum <*z*>) + (Sum y) is complex Element of COMPLEX
x is complex set
y is complex set
<*x,y*> is Relation-like NAT -defined Function-like non empty V45() 2 -element FinSequence-like FinSubsequence-like complex-valued set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,x] is set
{1,x} is V67() set
{1} is non empty trivial 1 -element V67() V68() V69() V70() V71() V72() set
{{1,x},{1}} is set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
<*y*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,y] is set
{1,y} is V67() set
{{1,y},{1}} is set
{[1,y]} is Relation-like Function-like constant non empty trivial 1 -element set
<*x*> ^ <*y*> is Relation-like NAT -defined Function-like non empty V45() 1 + 1 -element FinSequence-like FinSubsequence-like complex-valued set
1 + 1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
Sum <*x,y*> is complex set
x + y is complex Element of COMPLEX
z is complex Element of COMPLEX
<*z*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,z] is set
{1,z} is V67() set
{{1,z},{1}} is set
{[1,z]} is Relation-like Function-like constant non empty trivial 1 -element set
Sum <*z*> is complex Element of COMPLEX
addcomplex $$ <*z*> is complex Element of COMPLEX
(Sum <*z*>) + y is complex Element of COMPLEX
x is complex set
y is complex set
x + y is complex Element of COMPLEX
z is complex set
<*x,y,z*> is Relation-like NAT -defined Function-like non empty V45() 3 -element FinSequence-like FinSubsequence-like complex-valued set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,x] is set
{1,x} is V67() set
{1} is non empty trivial 1 -element V67() V68() V69() V70() V71() V72() set
{{1,x},{1}} is set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
<*y*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,y] is set
{1,y} is V67() set
{{1,y},{1}} is set
{[1,y]} is Relation-like Function-like constant non empty trivial 1 -element set
<*x*> ^ <*y*> is Relation-like NAT -defined Function-like non empty V45() 1 + 1 -element FinSequence-like FinSubsequence-like complex-valued set
1 + 1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
<*z*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,z] is set
{1,z} is V67() set
{{1,z},{1}} is set
{[1,z]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*x*> ^ <*y*>) ^ <*z*> is Relation-like NAT -defined Function-like non empty V45() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like complex-valued set
(1 + 1) + 1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
Sum <*x,y,z*> is complex set
(x + y) + z is complex Element of COMPLEX
<*x,y*> is Relation-like NAT -defined Function-like non empty V45() 2 -element FinSequence-like FinSubsequence-like complex-valued set
Sum <*x,y*> is complex set
(Sum <*x,y*>) + z is complex Element of COMPLEX
x is ordinal natural complex real V38() V45() cardinal set
y is complex set
x |-> y is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> y is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{y}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{y}:]
{y} is non empty trivial 1 -element V67() set
[:(Seg x),{y}:] is Relation-like complex-valued set
bool [:(Seg x),{y}:] is set
Sum (x |-> y) is complex set
x * y is complex Element of COMPLEX
z is complex Element of COMPLEX
x2 is ordinal natural complex real V38() V45() cardinal set
x2 |-> z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x2 -element FinSequence-like FinSubsequence-like complex-valued Element of x2 -tuples_on COMPLEX
x2 -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x2 } is set
Seg x2 is V45() x2 -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x2) ) } is set
(Seg x2) --> z is Relation-like Seg x2 -defined Seg x2 -defined COMPLEX -valued Function-like constant V14( Seg x2) V14( Seg x2) V18( Seg x2,{z}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x2),{z}:]
{z} is non empty trivial 1 -element V67() set
[:(Seg x2),{z}:] is Relation-like complex-valued set
bool [:(Seg x2),{z}:] is set
Sum (x2 |-> z) is complex Element of COMPLEX
addcomplex $$ (x2 |-> z) is complex Element of COMPLEX
x2 * z is complex Element of COMPLEX
x2 + 1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
(x2 + 1) |-> z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x2 + 1 -element FinSequence-like FinSubsequence-like complex-valued Element of (x2 + 1) -tuples_on COMPLEX
(x2 + 1) -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x2 + 1 } is set
Seg (x2 + 1) is V45() x2 + 1 -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x2 + 1) ) } is set
(Seg (x2 + 1)) --> z is Relation-like Seg (x2 + 1) -defined Seg (x2 + 1) -defined COMPLEX -valued Function-like constant V14( Seg (x2 + 1)) V14( Seg (x2 + 1)) V18( Seg (x2 + 1),{z}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg (x2 + 1)),{z}:]
[:(Seg (x2 + 1)),{z}:] is Relation-like complex-valued set
bool [:(Seg (x2 + 1)),{z}:] is set
Sum ((x2 + 1) |-> z) is complex Element of COMPLEX
addcomplex $$ ((x2 + 1) |-> z) is complex Element of COMPLEX
(x2 + 1) * z is complex Element of COMPLEX
<*z*> is Relation-like NAT -defined COMPLEX -valued Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
[1,z] is set
{1,z} is V67() set
{1} is non empty trivial 1 -element V67() V68() V69() V70() V71() V72() set
{{1,z},{1}} is set
{[1,z]} is Relation-like Function-like constant non empty trivial 1 -element set
(x2 |-> z) ^ <*z*> is Relation-like NAT -defined COMPLEX -valued Function-like non empty V45() x2 + 1 -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
x2 + 1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
Sum ((x2 |-> z) ^ <*z*>) is complex Element of COMPLEX
addcomplex $$ ((x2 |-> z) ^ <*z*>) is complex Element of COMPLEX
1 * z is complex Element of COMPLEX
(x2 * z) + (1 * z) is complex Element of COMPLEX
0 |-> z is Relation-like non-zero empty-yielding NAT -defined COMPLEX -valued Function-like one-to-one constant functional empty ordinal natural complex real V38() Function-yielding V44() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V67() V68() V69() V70() V71() V72() V73() Element of 0 -tuples_on COMPLEX
0 -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = 0 } is set
Seg 0 is Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ordinal natural complex real V38() Function-yielding V44() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V67() V68() V69() V70() V71() V72() V73() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1, 0 ) ) } is set
(Seg 0) --> z is Relation-like non-zero empty-yielding Seg 0 -defined Seg 0 -defined COMPLEX -valued RAT -valued Function-like one-to-one constant functional empty V14( Seg 0) V14( Seg 0) V18( Seg 0,{z}) ordinal natural complex real V38() Function-yielding V44() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V67() V68() V69() V70() V71() V72() V73() Element of bool [:(Seg 0),{z}:]
{z} is non empty trivial 1 -element V67() set
[:(Seg 0),{z}:] is Relation-like complex-valued set
bool [:(Seg 0),{z}:] is set
Sum (0 |-> z) is complex real V38() Element of COMPLEX
addcomplex $$ (0 |-> z) is complex Element of COMPLEX
0 * z is complex Element of COMPLEX
x is ordinal natural complex real V38() V45() cardinal set
x |-> 0c is Relation-like empty-yielding NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> 0c is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{0c}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{0c}:]
{0c} is non empty trivial 1 -element V67() set
[:(Seg x),{0c}:] is Relation-like complex-valued set
bool [:(Seg x),{0c}:] is set
Sum (x |-> 0c) is complex real V38() Element of COMPLEX
addcomplex $$ (x |-> 0c) is complex Element of COMPLEX
x * 0 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
x is complex set
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(y,x) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
x multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (x,(id COMPLEX)) is Relation-like Function-like set
y (#) (x multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
Sum (y,x) is complex Element of COMPLEX
addcomplex $$ (y,x) is complex Element of COMPLEX
Sum y is complex set
x * (Sum y) is complex Element of COMPLEX
x2 is complex Element of COMPLEX
multcomplex [;] (x2,(id COMPLEX)) is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex $$ z is complex Element of COMPLEX
(multcomplex [;] (x2,(id COMPLEX))) . (addcomplex $$ z) is complex Element of COMPLEX
Sum z is complex Element of COMPLEX
x * (Sum z) is complex Element of COMPLEX
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(x) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(- 1) (#) x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x (#) ((- 1) multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
Sum (x) is complex Element of COMPLEX
addcomplex $$ (x) is complex Element of COMPLEX
Sum x is complex set
- (Sum x) is complex Element of COMPLEX
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex $$ y is complex Element of COMPLEX
compcomplex . (addcomplex $$ y) is complex Element of COMPLEX
Sum y is complex Element of COMPLEX
- (Sum y) is complex Element of COMPLEX
x is ordinal natural complex real V38() V45() cardinal set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
Sum y is complex Element of COMPLEX
addcomplex $$ y is complex Element of COMPLEX
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
addcomplex .: (y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (y,z) is Relation-like Function-like set
Sum (x,y,z) is complex Element of COMPLEX
addcomplex $$ (x,y,z) is complex Element of COMPLEX
Sum z is complex Element of COMPLEX
addcomplex $$ z is complex Element of COMPLEX
(Sum y) + (Sum z) is complex Element of COMPLEX
x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex $$ x2 is complex Element of COMPLEX
y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
addcomplex $$ y2 is complex Element of COMPLEX
addcomplex . ((addcomplex $$ x2),(addcomplex $$ y2)) is complex Element of COMPLEX
[(addcomplex $$ x2),(addcomplex $$ y2)] is set
{(addcomplex $$ x2),(addcomplex $$ y2)} is V67() set
{(addcomplex $$ x2)} is non empty trivial 1 -element V67() set
{{(addcomplex $$ x2),(addcomplex $$ y2)},{(addcomplex $$ x2)}} is set
addcomplex . [(addcomplex $$ x2),(addcomplex $$ y2)] is complex set
x is ordinal natural complex real V38() V45() cardinal set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
Sum y is complex Element of COMPLEX
addcomplex $$ y is complex Element of COMPLEX
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
- z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z (#) ((- 1) multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
compcomplex * z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y + (- z) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (y,(- z)) is Relation-like Function-like set
diffcomplex .: (y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
diffcomplex .: (y,z) is Relation-like Function-like set
Sum (x,y,z) is complex Element of COMPLEX
addcomplex $$ (x,y,z) is complex Element of COMPLEX
Sum z is complex Element of COMPLEX
addcomplex $$ z is complex Element of COMPLEX
(Sum y) - (Sum z) is complex Element of COMPLEX
- (Sum z) is complex set
(Sum y) + (- (Sum z)) is set
(x,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
Sum (x,z) is complex Element of COMPLEX
addcomplex $$ (x,z) is complex Element of COMPLEX
(Sum y) + (Sum (x,z)) is complex Element of COMPLEX
Product (<*> COMPLEX) is complex real V38() Element of COMPLEX
multcomplex $$ (<*> COMPLEX) is complex Element of COMPLEX
x is Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ordinal natural complex real V38() Function-yielding V44() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V67() V68() V69() V70() V71() V72() V73() set
Product x is complex real V38() set
Product (<*> COMPLEX) is complex real V38() Element of COMPLEX
multcomplex $$ (<*> COMPLEX) is complex Element of COMPLEX
x is complex set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V45() 1 -element FinSequence-like FinSubsequence-like complex-valued set
[1,x] is set
{1,x} is V67() set
{1} is non empty trivial 1 -element V67() V68() V69() V70() V71() V72() set
{{1,x},{1}} is set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
<*x*> ^ y is Relation-like NAT -defined Function-like non empty V45() FinSequence-like FinSubsequence-like complex-valued set
Product (<*x*> ^ y) is complex set
Product y is complex set
x * (Product y) is complex Element of COMPLEX
Product <*x*> is complex set
(Product <*x*>) * (Product y) is complex Element of COMPLEX
0 -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = 0 } is set
x is Relation-like non-zero empty-yielding NAT -defined COMPLEX -valued Function-like one-to-one constant functional empty ordinal natural complex real V38() Function-yielding V44() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V67() V68() V69() V70() V71() V72() V73() Element of 0 -tuples_on COMPLEX
Product x is complex real V38() Element of COMPLEX
multcomplex $$ x is complex Element of COMPLEX
x is ordinal natural complex real V38() V45() cardinal set
y is ordinal natural complex real V38() V45() cardinal set
x + y is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
z is complex set
(x + y) |-> z is Relation-like NAT -defined Function-like V45() x + y -element FinSequence-like FinSubsequence-like complex-valued set
Seg (x + y) is V45() x + y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x + y) ) } is set
(Seg (x + y)) --> z is Relation-like Seg (x + y) -defined Seg (x + y) -defined Function-like constant V14( Seg (x + y)) V14( Seg (x + y)) V18( Seg (x + y),{z}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg (x + y)),{z}:]
{z} is non empty trivial 1 -element V67() set
[:(Seg (x + y)),{z}:] is Relation-like complex-valued set
bool [:(Seg (x + y)),{z}:] is set
Product ((x + y) |-> z) is complex set
x |-> z is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> z is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{z}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{z}:]
[:(Seg x),{z}:] is Relation-like complex-valued set
bool [:(Seg x),{z}:] is set
Product (x |-> z) is complex set
y |-> z is Relation-like NAT -defined Function-like V45() y -element FinSequence-like FinSubsequence-like complex-valued set
Seg y is V45() y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,y) ) } is set
(Seg y) --> z is Relation-like Seg y -defined Seg y -defined Function-like constant V14( Seg y) V14( Seg y) V18( Seg y,{z}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg y),{z}:]
[:(Seg y),{z}:] is Relation-like complex-valued set
bool [:(Seg y),{z}:] is set
Product (y |-> z) is complex set
(Product (x |-> z)) * (Product (y |-> z)) is complex Element of COMPLEX
x2 is complex Element of COMPLEX
(x + y) |-> x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x + y -element FinSequence-like FinSubsequence-like complex-valued Element of (x + y) -tuples_on COMPLEX
(x + y) -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x + y } is set
(Seg (x + y)) --> x2 is Relation-like Seg (x + y) -defined Seg (x + y) -defined COMPLEX -valued Function-like constant V14( Seg (x + y)) V14( Seg (x + y)) V18( Seg (x + y),{x2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg (x + y)),{x2}:]
{x2} is non empty trivial 1 -element V67() set
[:(Seg (x + y)),{x2}:] is Relation-like complex-valued set
bool [:(Seg (x + y)),{x2}:] is set
Product ((x + y) |-> x2) is complex Element of COMPLEX
multcomplex $$ ((x + y) |-> x2) is complex Element of COMPLEX
x |-> x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
(Seg x) --> x2 is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{x2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{x2}:]
[:(Seg x),{x2}:] is Relation-like complex-valued set
bool [:(Seg x),{x2}:] is set
multcomplex $$ (x |-> x2) is complex Element of COMPLEX
y |-> x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() y -element FinSequence-like FinSubsequence-like complex-valued Element of y -tuples_on COMPLEX
y -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = y } is set
(Seg y) --> x2 is Relation-like Seg y -defined Seg y -defined COMPLEX -valued Function-like constant V14( Seg y) V14( Seg y) V18( Seg y,{x2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg y),{x2}:]
[:(Seg y),{x2}:] is Relation-like complex-valued set
bool [:(Seg y),{x2}:] is set
multcomplex $$ (y |-> x2) is complex Element of COMPLEX
multcomplex . ((multcomplex $$ (x |-> x2)),(multcomplex $$ (y |-> x2))) is complex Element of COMPLEX
[(multcomplex $$ (x |-> x2)),(multcomplex $$ (y |-> x2))] is set
{(multcomplex $$ (x |-> x2)),(multcomplex $$ (y |-> x2))} is V67() set
{(multcomplex $$ (x |-> x2))} is non empty trivial 1 -element V67() set
{{(multcomplex $$ (x |-> x2)),(multcomplex $$ (y |-> x2))},{(multcomplex $$ (x |-> x2))}} is set
multcomplex . [(multcomplex $$ (x |-> x2)),(multcomplex $$ (y |-> x2))] is complex set
Product (x |-> x2) is complex Element of COMPLEX
Product (y |-> x2) is complex Element of COMPLEX
(Product (x |-> x2)) * (Product (y |-> x2)) is complex Element of COMPLEX
x is ordinal natural complex real V38() V45() cardinal set
y is ordinal natural complex real V38() V45() cardinal set
x * y is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
z is complex set
(x * y) |-> z is Relation-like NAT -defined Function-like V45() x * y -element FinSequence-like FinSubsequence-like complex-valued set
Seg (x * y) is V45() x * y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x * y) ) } is set
(Seg (x * y)) --> z is Relation-like Seg (x * y) -defined Seg (x * y) -defined Function-like constant V14( Seg (x * y)) V14( Seg (x * y)) V18( Seg (x * y),{z}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg (x * y)),{z}:]
{z} is non empty trivial 1 -element V67() set
[:(Seg (x * y)),{z}:] is Relation-like complex-valued set
bool [:(Seg (x * y)),{z}:] is set
Product ((x * y) |-> z) is complex set
x |-> z is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> z is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{z}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{z}:]
[:(Seg x),{z}:] is Relation-like complex-valued set
bool [:(Seg x),{z}:] is set
Product (x |-> z) is complex set
y |-> (Product (x |-> z)) is Relation-like NAT -defined Function-like V45() y -element FinSequence-like FinSubsequence-like complex-valued set
Seg y is V45() y -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,y) ) } is set
(Seg y) --> (Product (x |-> z)) is Relation-like Seg y -defined Seg y -defined Function-like constant V14( Seg y) V14( Seg y) V18( Seg y,{(Product (x |-> z))}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg y),{(Product (x |-> z))}:]
{(Product (x |-> z))} is non empty trivial 1 -element V67() set
[:(Seg y),{(Product (x |-> z))}:] is Relation-like complex-valued set
bool [:(Seg y),{(Product (x |-> z))}:] is set
Product (y |-> (Product (x |-> z))) is complex set
x2 is complex Element of COMPLEX
(x * y) |-> x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x * y -element FinSequence-like FinSubsequence-like complex-valued Element of (x * y) -tuples_on COMPLEX
(x * y) -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x * y } is set
(Seg (x * y)) --> x2 is Relation-like Seg (x * y) -defined Seg (x * y) -defined COMPLEX -valued Function-like constant V14( Seg (x * y)) V14( Seg (x * y)) V18( Seg (x * y),{x2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg (x * y)),{x2}:]
{x2} is non empty trivial 1 -element V67() set
[:(Seg (x * y)),{x2}:] is Relation-like complex-valued set
bool [:(Seg (x * y)),{x2}:] is set
Product ((x * y) |-> x2) is complex Element of COMPLEX
multcomplex $$ ((x * y) |-> x2) is complex Element of COMPLEX
x |-> x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
(Seg x) --> x2 is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{x2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{x2}:]
[:(Seg x),{x2}:] is Relation-like complex-valued set
bool [:(Seg x),{x2}:] is set
Product (x |-> x2) is complex Element of COMPLEX
multcomplex $$ (x |-> x2) is complex Element of COMPLEX
y |-> (Product (x |-> x2)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() y -element FinSequence-like FinSubsequence-like complex-valued Element of y -tuples_on COMPLEX
y -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = y } is set
(Seg y) --> (Product (x |-> x2)) is Relation-like Seg y -defined Seg y -defined COMPLEX -valued Function-like constant V14( Seg y) V14( Seg y) V18( Seg y,{(Product (x |-> x2))}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg y),{(Product (x |-> x2))}:]
{(Product (x |-> x2))} is non empty trivial 1 -element V67() set
[:(Seg y),{(Product (x |-> x2))}:] is Relation-like complex-valued set
bool [:(Seg y),{(Product (x |-> x2))}:] is set
Product (y |-> (Product (x |-> x2))) is complex Element of COMPLEX
multcomplex $$ (y |-> (Product (x |-> x2))) is complex Element of COMPLEX
x is ordinal natural complex real V38() V45() cardinal set
y is complex set
x |-> y is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> y is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{y}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{y}:]
{y} is non empty trivial 1 -element V67() set
[:(Seg x),{y}:] is Relation-like complex-valued set
bool [:(Seg x),{y}:] is set
Product (x |-> y) is complex set
z is complex set
y * z is complex Element of COMPLEX
x |-> (y * z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
(Seg x) --> (y * z) is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{(y * z)}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{(y * z)}:]
{(y * z)} is non empty trivial 1 -element V67() set
[:(Seg x),{(y * z)}:] is Relation-like complex-valued set
bool [:(Seg x),{(y * z)}:] is set
Product (x |-> (y * z)) is complex Element of COMPLEX
multcomplex $$ (x |-> (y * z)) is complex Element of COMPLEX
x |-> z is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
(Seg x) --> z is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{z}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{z}:]
{z} is non empty trivial 1 -element V67() set
[:(Seg x),{z}:] is Relation-like complex-valued set
bool [:(Seg x),{z}:] is set
Product (x |-> z) is complex set
(Product (x |-> y)) * (Product (x |-> z)) is complex Element of COMPLEX
x2 is complex Element of COMPLEX
y2 is complex Element of COMPLEX
x2 * y2 is complex Element of COMPLEX
x |-> (x2 * y2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> (x2 * y2) is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{(x2 * y2)}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{(x2 * y2)}:]
{(x2 * y2)} is non empty trivial 1 -element V67() set
[:(Seg x),{(x2 * y2)}:] is Relation-like complex-valued set
bool [:(Seg x),{(x2 * y2)}:] is set
Product (x |-> (x2 * y2)) is complex Element of COMPLEX
multcomplex $$ (x |-> (x2 * y2)) is complex Element of COMPLEX
multcomplex . (x2,y2) is complex Element of COMPLEX
[x2,y2] is set
{x2,y2} is V67() set
{x2} is non empty trivial 1 -element V67() set
{{x2,y2},{x2}} is set
multcomplex . [x2,y2] is complex set
x |-> (multcomplex . (x2,y2)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> (multcomplex . (x2,y2)) is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{(multcomplex . (x2,y2))}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{(multcomplex . (x2,y2))}:]
{(multcomplex . (x2,y2))} is non empty trivial 1 -element V67() set
[:(Seg x),{(multcomplex . (x2,y2))}:] is Relation-like complex-valued set
bool [:(Seg x),{(multcomplex . (x2,y2))}:] is set
multcomplex $$ (x |-> (multcomplex . (x2,y2))) is complex Element of COMPLEX
x |-> x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> x2 is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{x2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{x2}:]
[:(Seg x),{x2}:] is Relation-like complex-valued set
bool [:(Seg x),{x2}:] is set
multcomplex $$ (x |-> x2) is complex Element of COMPLEX
x |-> y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> y2 is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{y2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{y2}:]
{y2} is non empty trivial 1 -element V67() set
[:(Seg x),{y2}:] is Relation-like complex-valued set
bool [:(Seg x),{y2}:] is set
multcomplex $$ (x |-> y2) is complex Element of COMPLEX
multcomplex . ((multcomplex $$ (x |-> x2)),(multcomplex $$ (x |-> y2))) is complex Element of COMPLEX
[(multcomplex $$ (x |-> x2)),(multcomplex $$ (x |-> y2))] is set
{(multcomplex $$ (x |-> x2)),(multcomplex $$ (x |-> y2))} is V67() set
{(multcomplex $$ (x |-> x2))} is non empty trivial 1 -element V67() set
{{(multcomplex $$ (x |-> x2)),(multcomplex $$ (x |-> y2))},{(multcomplex $$ (x |-> x2))}} is set
multcomplex . [(multcomplex $$ (x |-> x2)),(multcomplex $$ (x |-> y2))] is complex set
Product (x |-> x2) is complex Element of COMPLEX
Product (x |-> y2) is complex Element of COMPLEX
(Product (x |-> x2)) * (Product (x |-> y2)) is complex Element of COMPLEX
x is ordinal natural complex real V38() V45() cardinal set
y is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
Product y is complex Element of COMPLEX
multcomplex $$ y is complex Element of COMPLEX
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
multcomplex .: (y,z) is Relation-like Function-like set
Product (x,y,z) is complex Element of COMPLEX
multcomplex $$ (x,y,z) is complex Element of COMPLEX
Product z is complex Element of COMPLEX
multcomplex $$ z is complex Element of COMPLEX
(Product y) * (Product z) is complex Element of COMPLEX
x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
multcomplex $$ x2 is complex Element of COMPLEX
y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
multcomplex $$ y2 is complex Element of COMPLEX
multcomplex . ((multcomplex $$ x2),(multcomplex $$ y2)) is complex Element of COMPLEX
[(multcomplex $$ x2),(multcomplex $$ y2)] is set
{(multcomplex $$ x2),(multcomplex $$ y2)} is V67() set
{(multcomplex $$ x2)} is non empty trivial 1 -element V67() set
{{(multcomplex $$ x2),(multcomplex $$ y2)},{(multcomplex $$ x2)}} is set
multcomplex . [(multcomplex $$ x2),(multcomplex $$ y2)] is complex set
x is ordinal natural complex real V38() V45() cardinal set
y is complex set
x |-> y is Relation-like NAT -defined Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued set
Seg x is V45() x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1,x) ) } is set
(Seg x) --> y is Relation-like Seg x -defined Seg x -defined Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{y}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{y}:]
{y} is non empty trivial 1 -element V67() set
[:(Seg x),{y}:] is Relation-like complex-valued set
bool [:(Seg x),{y}:] is set
Product (x |-> y) is complex set
z is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(x,z,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
x -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = x } is set
y multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (y,(id COMPLEX)) is Relation-like Function-like set
(y multcomplex) * z is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
z (#) (y multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
Product (x,z,y) is complex Element of COMPLEX
multcomplex $$ (x,z,y) is complex Element of COMPLEX
Product z is complex Element of COMPLEX
multcomplex $$ z is complex Element of COMPLEX
(Product (x |-> y)) * (Product z) is complex Element of COMPLEX
x2 is complex Element of COMPLEX
x |-> x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
(Seg x) --> x2 is Relation-like Seg x -defined Seg x -defined COMPLEX -valued Function-like constant V14( Seg x) V14( Seg x) V18( Seg x,{x2}) V45() FinSequence-like FinSubsequence-like complex-valued Element of bool [:(Seg x),{x2}:]
{x2} is non empty trivial 1 -element V67() set
[:(Seg x),{x2}:] is Relation-like complex-valued set
bool [:(Seg x),{x2}:] is set
(x,(x |-> x2),z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() x -element FinSequence-like FinSubsequence-like complex-valued Element of x -tuples_on COMPLEX
multcomplex .: ((x |-> x2),z) is Relation-like Function-like set
Product (x,(x |-> x2),z) is complex Element of COMPLEX
multcomplex $$ (x,(x |-> x2),z) is complex Element of COMPLEX
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(x) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
(- 1) (#) x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x (#) ((- 1) multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
len (x) is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
len x is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
dom (x) is V67() V68() V69() V70() V71() V72() Element of bool NAT
dom x is V67() V68() V69() V70() V71() V72() Element of bool NAT
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
len x is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
len y is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
(x,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (x,y) is Relation-like Function-like set
len (x,y) is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
(len x) -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = len x } is set
x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() len x -element FinSequence-like FinSubsequence-like complex-valued Element of (len x) -tuples_on COMPLEX
y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() len x -element FinSequence-like FinSubsequence-like complex-valued Element of (len x) -tuples_on COMPLEX
((len x),x2,y2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() len x -element FinSequence-like FinSubsequence-like complex-valued Element of (len x) -tuples_on COMPLEX
addcomplex .: (x2,y2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (x2,y2) is Relation-like Function-like set
dom ((len x),x2,y2) is len x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
Seg (len x) is V45() len x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1, len x) ) } is set
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
len x is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
len y is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
(x,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
- y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y (#) ((- 1) multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
y (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x + (- y) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (x,(- y)) is Relation-like Function-like set
diffcomplex .: (x,y) is Relation-like Function-like set
len (x,y) is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
(len x) -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = len x } is set
x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() len x -element FinSequence-like FinSubsequence-like complex-valued Element of (len x) -tuples_on COMPLEX
y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() len x -element FinSequence-like FinSubsequence-like complex-valued Element of (len x) -tuples_on COMPLEX
((len x),x2,y2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() len x -element FinSequence-like FinSubsequence-like complex-valued Element of (len x) -tuples_on COMPLEX
- y2 is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(- 1) (#) y2 is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
((- 1) multcomplex) * y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
y2 (#) ((- 1) multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
compcomplex * y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
y2 (#) compcomplex is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
x2 + (- y2) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
addcomplex .: (x2,(- y2)) is Relation-like Function-like set
diffcomplex .: (x2,y2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
diffcomplex .: (x2,y2) is Relation-like Function-like set
dom ((len x),x2,y2) is len x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
Seg (len x) is V45() len x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1, len x) ) } is set
x is complex real V38() set
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
(y,x) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
x multcomplex is Relation-like Function-like non empty V14( COMPLEX ) V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]
multcomplex [;] (x,(id COMPLEX)) is Relation-like Function-like set
y (#) (x multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
len (y,x) is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
len y is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
(len y) -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = len y } is set
x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() len y -element FinSequence-like FinSubsequence-like complex-valued Element of (len y) -tuples_on COMPLEX
((len y),x2,x) is Relation-like NAT -defined COMPLEX -valued Function-like V45() len y -element FinSequence-like FinSubsequence-like complex-valued Element of (len y) -tuples_on COMPLEX
(x multcomplex) * x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
x2 (#) (x multcomplex) is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
len ((len y),x2,x) is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
x is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
len x is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
y is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
len y is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
z is Relation-like NAT -defined Function-like V45() FinSequence-like FinSubsequence-like complex-valued set
len z is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
(x,y) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (x,y) is Relation-like Function-like set
((x,y),z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
multcomplex .: ((x,y),z) is Relation-like Function-like set
(x,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
multcomplex .: (x,z) is Relation-like Function-like set
(y,z) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
multcomplex .: (y,z) is Relation-like Function-like set
((x,z),(y,z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((x,z),(y,z)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: ((x,z),(y,z)) is Relation-like Function-like set
(len x) -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ b1 where b1 is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = len x } is set
dom ((x,y),z) is V67() V68() V69() V70() V71() V72() Element of bool NAT
x2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() len x -element FinSequence-like FinSubsequence-like complex-valued Element of (len x) -tuples_on COMPLEX
y2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() len x -element FinSequence-like FinSubsequence-like complex-valued Element of (len x) -tuples_on COMPLEX
((len x),x2,y2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() len x -element FinSequence-like FinSubsequence-like complex-valued Element of (len x) -tuples_on COMPLEX
addcomplex .: (x2,y2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (x2,y2) is Relation-like Function-like set
z2 is Relation-like NAT -defined COMPLEX -valued Function-like V45() len x -element FinSequence-like FinSubsequence-like complex-valued Element of (len x) -tuples_on COMPLEX
((len x),((len x),x2,y2),z2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() len x -element FinSequence-like FinSubsequence-like complex-valued Element of (len x) -tuples_on COMPLEX
multcomplex .: (((len x),x2,y2),z2) is Relation-like Function-like set
len ((len x),((len x),x2,y2),z2) is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
Seg (len ((len x),((len x),x2,y2),z2)) is V45() len ((len x),((len x),x2,y2),z2) -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1, len ((len x),((len x),x2,y2),z2)) ) } is set
Seg (len x) is V45() len x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1, len x) ) } is set
((len x),x2,z2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() len x -element FinSequence-like FinSubsequence-like complex-valued Element of (len x) -tuples_on COMPLEX
multcomplex .: (x2,z2) is Relation-like Function-like set
((len x),y2,z2) is Relation-like NAT -defined COMPLEX -valued Function-like V45() len x -element FinSequence-like FinSubsequence-like complex-valued Element of (len x) -tuples_on COMPLEX
multcomplex .: (y2,z2) is Relation-like Function-like set
((len x),((len x),x2,z2),((len x),y2,z2)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() len x -element FinSequence-like FinSubsequence-like complex-valued Element of (len x) -tuples_on COMPLEX
addcomplex .: (((len x),x2,z2),((len x),y2,z2)) is Relation-like NAT -defined COMPLEX -valued Function-like V45() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex .: (((len x),x2,z2),((len x),y2,z2)) is Relation-like Function-like set
len ((len x),((len x),x2,z2),((len x),y2,z2)) is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
Seg (len ((len x),((len x),x2,z2),((len x),y2,z2))) is V45() len ((len x),((len x),x2,z2),((len x),y2,z2)) -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1, len ((len x),((len x),x2,z2),((len x),y2,z2))) ) } is set
dom ((len x),((len x),x2,z2),((len x),y2,z2)) is len x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
dom (x,z) is V67() V68() V69() V70() V71() V72() Element of bool NAT
len ((len x),x2,z2) is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
Seg (len ((len x),x2,z2)) is V45() len ((len x),x2,z2) -element V67() V68() V69() V70() V71() V72() Element of bool NAT
{ b1 where b1 is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT : ( R27(1,b1) & R27(b1, len ((len x),x2,z2)) ) } is set
i is ordinal natural complex real V38() V45() cardinal set
((x,y),z) . i is complex set
((x,z),(y,z)) . i is complex set
x . i is complex set
y . i is complex set
(x,y) . i is complex set
z . i is complex set
len ((len x),x2,y2) is ordinal natural complex real V38() V41() V42() V45() cardinal V67() V68() V69() V70() V71() V72() Element of NAT
dom ((len x),x2,y2) is len x -element V67() V68() V69() V70() V71() V72() Element of bool NAT
(x . i) + (y . i) is complex Element of COMPLEX
((x,y) . i) * (z . i) is complex Element of COMPLEX
(x . i) * (z . i) is complex Element of COMPLEX
(y . i) * (z . i) is complex Element of COMPLEX
((x . i) * (z . i)) + ((y . i) * (z . i)) is complex Element of COMPLEX
(x,z) . i is complex set
((x,z) . i) + ((y . i) * (z . i)) is complex Element of COMPLEX
(y,z) . i is complex set
((x,z) . i) + ((y,z) . i) is complex Element of COMPLEX