:: RVSUM_1 semantic presentation

REAL is non empty V53() V54() V55() V59() V60() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V53() V54() V55() V56() V57() V58() V59() V60() cardinal limit_cardinal Element of bool REAL

bool REAL is V60() set

RAT is non empty V53() V54() V55() V56() V59() V60() set

0 is Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V41() complex-valued ext-real-valued real-valued natural-valued V53() V54() V55() V56() V57() V58() V59() V60() Function-yielding V70() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered set

COMPLEX is non empty V53() V59() V60() set

INT is non empty V53() V54() V55() V56() V57() V59() V60() set

[:COMPLEX,COMPLEX:] is Relation-like complex-valued V60() set

bool [:COMPLEX,COMPLEX:] is V60() set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like complex-valued V60() set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is V60() set

[:REAL,REAL:] is Relation-like complex-valued ext-real-valued real-valued V60() set

bool [:REAL,REAL:] is V60() set

[:[:REAL,REAL:],REAL:] is Relation-like complex-valued ext-real-valued real-valued V60() set

bool [:[:REAL,REAL:],REAL:] is V60() set

[:RAT,RAT:] is Relation-like RAT -valued complex-valued ext-real-valued real-valued V60() set

bool [:RAT,RAT:] is V60() set

[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued complex-valued ext-real-valued real-valued V60() set

bool [:[:RAT,RAT:],RAT:] is V60() set

[:INT,INT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued V60() set

bool [:INT,INT:] is V60() set

[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued V60() set

bool [:[:INT,INT:],INT:] is V60() set

[:NAT,NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued V60() set

[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued V60() set

bool [:[:NAT,NAT:],NAT:] is V60() set

omega is non empty epsilon-transitive epsilon-connected ordinal V53() V54() V55() V56() V57() V58() V59() V60() cardinal limit_cardinal set

bool omega is V60() set

bool NAT is V60() set

K101(NAT) is V27() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT

2 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT

0 is Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V41() V42() complex-valued ext-real-valued real-valued natural-valued V53() V54() V55() V56() V57() V58() V59() V60() Function-yielding V70() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

4 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT

5 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT

addcomplex is Relation-like Function-like V14([:COMPLEX,COMPLEX:]) V18([:COMPLEX,COMPLEX:], COMPLEX ) commutative associative having_a_unity complex-valued Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]

multcomplex is Relation-like Function-like V14([:COMPLEX,COMPLEX:]) V18([:COMPLEX,COMPLEX:], COMPLEX ) commutative associative having_a_unity complex-valued Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]

compreal is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

addreal is Relation-like Function-like V14([:REAL,REAL:]) V18([:REAL,REAL:], REAL ) commutative associative having_a_unity complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

diffreal is Relation-like Function-like V14([:REAL,REAL:]) V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

multreal is Relation-like Function-like V14([:REAL,REAL:]) V18([:REAL,REAL:], REAL ) commutative associative having_a_unity complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

the_unity_wrt addcomplex is complex Element of COMPLEX

the_unity_wrt addreal is complex ext-real real Element of REAL

the_unity_wrt multcomplex is complex Element of COMPLEX

the_unity_wrt multreal is complex ext-real real Element of REAL

card 0 is Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V41() complex-valued ext-real-valued real-valued natural-valued V53() V54() V55() V56() V57() V58() V59() V60() Function-yielding V70() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered set

F is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V60() cardinal set

F |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on NAT

F -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT

NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT

{ b

Seg F is V53() V54() V55() V56() V57() V58() V60() F -element Element of bool NAT

{ b

(Seg F) --> 0 is Relation-like Seg F -defined Seg F -defined NAT -valued RAT -valued INT -valued Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{0}) complex-valued ext-real-valued real-valued natural-valued V60() Function-yielding V70() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{0}:]

{0} is functional non empty trivial V53() V54() V55() V56() V57() V58() 1 -element set

[:(Seg F),{0}:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:(Seg F),{0}:] is set

the Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

F is Relation-like complex-valued ext-real-valued real-valued set

rng F is V53() V54() V55() set

F is non empty set

[:REAL,F:] is Relation-like V60() set

bool [:REAL,F:] is V60() set

i is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

g is Relation-like Function-like non empty V14( REAL ) V18( REAL ,F) Element of bool [:REAL,F:]

i (#) g is Relation-like NAT -defined Function-like set

dom i is V53() V54() V55() V56() V57() V58() Element of bool NAT

j is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V60() cardinal set

Seg j is V53() V54() V55() V56() V57() V58() V60() j -element Element of bool NAT

{ b

dom (i (#) g) is V53() V54() V55() V56() V57() V58() set

dom g is non empty set

(i) is V53() V54() V55() Element of bool REAL

F is complex ext-real real set

<*F*> is Relation-like NAT -defined Function-like constant non empty trivial V60() 1 -element FinSequence-like FinSubsequence-like set

[1,F] is set

{1,F} is non empty V53() V54() V55() set

{1} is non empty trivial V53() V54() V55() V56() V57() V58() 1 -element set

{{1,F},{1}} is non empty set

{[1,F]} is Relation-like Function-like constant non empty trivial 1 -element set

g is complex ext-real real Element of REAL

<*g*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL

[1,g] is set

{1,g} is non empty V53() V54() V55() set

{{1,g},{1}} is non empty set

{[1,g]} is Relation-like Function-like constant non empty trivial 1 -element set

F is complex ext-real real set

g is complex ext-real real set

<*F,g*> is Relation-like NAT -defined Function-like non empty V60() 2 -element FinSequence-like FinSubsequence-like set

<*F*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,F] is set

{1,F} is non empty V53() V54() V55() set

{{1,F},{1}} is non empty set

{[1,F]} is Relation-like Function-like constant non empty trivial 1 -element set

<*g*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,g] is set

{1,g} is non empty V53() V54() V55() set

{{1,g},{1}} is non empty set

{[1,g]} is Relation-like Function-like constant non empty trivial 1 -element set

<*F*> ^ <*g*> is Relation-like NAT -defined Function-like non empty V60() 1 + 1 -element FinSequence-like FinSubsequence-like set

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT

i is complex ext-real real Element of REAL

j is complex ext-real real Element of REAL

<*i,j*> is Relation-like NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued V60() 2 -element FinSequence-like FinSubsequence-like FinSequence of REAL

<*i*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,i] is set

{1,i} is non empty V53() V54() V55() set

{{1,i},{1}} is non empty set

{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set

<*j*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,j] is set

{1,j} is non empty V53() V54() V55() set

{{1,j},{1}} is non empty set

{[1,j]} is Relation-like Function-like constant non empty trivial 1 -element set

<*i*> ^ <*j*> is Relation-like NAT -defined Function-like non empty V60() 1 + 1 -element FinSequence-like FinSubsequence-like set

F is complex ext-real real set

g is complex ext-real real set

i is complex ext-real real set

<*F,g,i*> is Relation-like NAT -defined Function-like non empty V60() 3 -element FinSequence-like FinSubsequence-like set

<*F*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,F] is set

{1,F} is non empty V53() V54() V55() set

{{1,F},{1}} is non empty set

{[1,F]} is Relation-like Function-like constant non empty trivial 1 -element set

<*g*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,g] is set

{1,g} is non empty V53() V54() V55() set

{{1,g},{1}} is non empty set

{[1,g]} is Relation-like Function-like constant non empty trivial 1 -element set

<*F*> ^ <*g*> is Relation-like NAT -defined Function-like non empty V60() 1 + 1 -element FinSequence-like FinSubsequence-like set

<*i*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,i] is set

{1,i} is non empty V53() V54() V55() set

{{1,i},{1}} is non empty set

{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set

(<*F*> ^ <*g*>) ^ <*i*> is Relation-like NAT -defined Function-like non empty V60() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set

(1 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT

j is complex ext-real real Element of REAL

q2 is complex ext-real real Element of REAL

p3 is complex ext-real real Element of REAL

<*j,q2,p3*> is Relation-like NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued V60() 3 -element FinSequence-like FinSubsequence-like FinSequence of REAL

<*j*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,j] is set

{1,j} is non empty V53() V54() V55() set

{{1,j},{1}} is non empty set

{[1,j]} is Relation-like Function-like constant non empty trivial 1 -element set

<*q2*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,q2] is set

{1,q2} is non empty V53() V54() V55() set

{{1,q2},{1}} is non empty set

{[1,q2]} is Relation-like Function-like constant non empty trivial 1 -element set

<*j*> ^ <*q2*> is Relation-like NAT -defined Function-like non empty V60() 1 + 1 -element FinSequence-like FinSubsequence-like set

<*p3*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,p3] is set

{1,p3} is non empty V53() V54() V55() set

{{1,p3},{1}} is non empty set

{[1,p3]} is Relation-like Function-like constant non empty trivial 1 -element set

(<*j*> ^ <*q2*>) ^ <*p3*> is Relation-like NAT -defined Function-like non empty V60() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set

F is complex ext-real real set

g is complex ext-real real set

i is complex ext-real real set

j is complex ext-real real set

<*F,g,i,j*> is Relation-like NAT -defined Function-like non empty V60() 4 -element FinSequence-like FinSubsequence-like set

<*F,g,i*> is Relation-like NAT -defined Function-like non empty complex-valued ext-real-valued real-valued V60() 3 -element FinSequence-like FinSubsequence-like set

<*F*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,F] is set

{1,F} is non empty V53() V54() V55() set

{{1,F},{1}} is non empty set

{[1,F]} is Relation-like Function-like constant non empty trivial 1 -element set

<*g*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,g] is set

{1,g} is non empty V53() V54() V55() set

{{1,g},{1}} is non empty set

{[1,g]} is Relation-like Function-like constant non empty trivial 1 -element set

<*F*> ^ <*g*> is Relation-like NAT -defined Function-like non empty V60() 1 + 1 -element FinSequence-like FinSubsequence-like set

<*i*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,i] is set

{1,i} is non empty V53() V54() V55() set

{{1,i},{1}} is non empty set

{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set

(<*F*> ^ <*g*>) ^ <*i*> is Relation-like NAT -defined Function-like non empty V60() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set

<*j*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,j] is set

{1,j} is non empty V53() V54() V55() set

{{1,j},{1}} is non empty set

{[1,j]} is Relation-like Function-like constant non empty trivial 1 -element set

<*F,g,i*> ^ <*j*> is Relation-like NAT -defined Function-like non empty V60() 3 + 1 -element FinSequence-like FinSubsequence-like set

3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real V41() V42() V53() V54() V55() V56() V57() V58() V60() cardinal Element of NAT

q2 is complex ext-real real Element of REAL

p3 is complex ext-real real Element of REAL

f3 is complex ext-real real Element of REAL

a is complex ext-real real Element of REAL

<*q2,p3,f3,a*> is Relation-like NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued V60() 4 -element FinSequence-like FinSubsequence-like FinSequence of REAL

<*q2,p3,f3*> is Relation-like NAT -defined Function-like non empty complex-valued ext-real-valued real-valued V60() 3 -element FinSequence-like FinSubsequence-like set

<*q2*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,q2] is set

{1,q2} is non empty V53() V54() V55() set

{{1,q2},{1}} is non empty set

{[1,q2]} is Relation-like Function-like constant non empty trivial 1 -element set

<*p3*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,p3] is set

{1,p3} is non empty V53() V54() V55() set

{{1,p3},{1}} is non empty set

{[1,p3]} is Relation-like Function-like constant non empty trivial 1 -element set

<*q2*> ^ <*p3*> is Relation-like NAT -defined Function-like non empty V60() 1 + 1 -element FinSequence-like FinSubsequence-like set

<*f3*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,f3] is set

{1,f3} is non empty V53() V54() V55() set

{{1,f3},{1}} is non empty set

{[1,f3]} is Relation-like Function-like constant non empty trivial 1 -element set

(<*q2*> ^ <*p3*>) ^ <*f3*> is Relation-like NAT -defined Function-like non empty V60() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set

<*a*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,a] is set

{1,a} is non empty V53() V54() V55() set

{{1,a},{1}} is non empty set

{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set

<*q2,p3,f3*> ^ <*a*> is Relation-like NAT -defined Function-like non empty V60() 3 + 1 -element FinSequence-like FinSubsequence-like set

F is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V60() cardinal set

g is complex ext-real real set

F |-> g is Relation-like NAT -defined Function-like V60() F -element FinSequence-like FinSubsequence-like set

Seg F is V53() V54() V55() V56() V57() V58() V60() F -element Element of bool NAT

{ b

(Seg F) --> g is Relation-like Seg F -defined Seg F -defined Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{g}) complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{g}:]

{g} is non empty trivial V53() V54() V55() 1 -element set

[:(Seg F),{g}:] is Relation-like complex-valued ext-real-valued real-valued set

bool [:(Seg F),{g}:] is set

F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

F ^ g is Relation-like NAT -defined Function-like V60() FinSequence-like FinSubsequence-like set

rng (F ^ g) is set

(F) is V53() V54() V55() Element of bool REAL

(g) is V53() V54() V55() Element of bool REAL

(F) \/ (g) is V53() V54() V55() set

id REAL is Relation-like REAL -defined REAL -valued Function-like one-to-one non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued V47() non-decreasing Element of bool [:REAL,REAL:]

addreal * ((id REAL),compreal) is Relation-like Function-like V14([:REAL,REAL:]) V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

F is Relation-like Function-like V14([:REAL,REAL:]) V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

g is complex ext-real real Element of REAL

i is complex ext-real real Element of REAL

diffreal . (g,i) is complex ext-real real Element of REAL

[g,i] is set

{g,i} is non empty V53() V54() V55() set

{g} is non empty trivial V53() V54() V55() 1 -element set

{{g,i},{g}} is non empty set

diffreal . [g,i] is complex ext-real real set

g - i is complex ext-real real Element of REAL

- i is complex ext-real real Element of REAL

g + (- i) is complex ext-real real Element of REAL

addreal . (g,(- i)) is complex ext-real real Element of REAL

[g,(- i)] is set

{g,(- i)} is non empty V53() V54() V55() set

{{g,(- i)},{g}} is non empty set

addreal . [g,(- i)] is complex ext-real real set

compreal . i is complex ext-real real Element of REAL

addreal . (g,(compreal . i)) is complex ext-real real Element of REAL

[g,(compreal . i)] is set

{g,(compreal . i)} is non empty V53() V54() V55() set

{{g,(compreal . i)},{g}} is non empty set

addreal . [g,(compreal . i)] is complex ext-real real set

(addreal * ((id REAL),compreal)) . (g,i) is complex ext-real real Element of REAL

(addreal * ((id REAL),compreal)) . [g,i] is complex ext-real real set

F is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

g is complex ext-real real set

F . g is complex ext-real real Element of REAL

g ^2 is complex ext-real real set

g * g is complex ext-real real set

F is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

g is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

i is complex ext-real real Element of REAL

F . i is complex ext-real real Element of REAL

i ^2 is complex ext-real real Element of REAL

i * i is complex ext-real real set

g . i is complex ext-real real Element of REAL

() is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

F is complex ext-real real Element of REAL

g is complex ext-real real Element of REAL

i is complex ext-real real Element of REAL

addreal . (g,i) is complex ext-real real Element of REAL

[g,i] is set

{g,i} is non empty V53() V54() V55() set

{g} is non empty trivial V53() V54() V55() 1 -element set

{{g,i},{g}} is non empty set

addreal . [g,i] is complex ext-real real set

multreal . (F,(addreal . (g,i))) is complex ext-real real Element of REAL

[F,(addreal . (g,i))] is set

{F,(addreal . (g,i))} is non empty V53() V54() V55() set

{F} is non empty trivial V53() V54() V55() 1 -element set

{{F,(addreal . (g,i))},{F}} is non empty set

multreal . [F,(addreal . (g,i))] is complex ext-real real set

g + i is complex ext-real real Element of REAL

multreal . (F,(g + i)) is complex ext-real real Element of REAL

[F,(g + i)] is set

{F,(g + i)} is non empty V53() V54() V55() set

{{F,(g + i)},{F}} is non empty set

multreal . [F,(g + i)] is complex ext-real real set

F * (g + i) is complex ext-real real Element of REAL

F * g is complex ext-real real Element of REAL

F * i is complex ext-real real Element of REAL

(F * g) + (F * i) is complex ext-real real Element of REAL

addreal . ((F * g),(F * i)) is complex ext-real real Element of REAL

[(F * g),(F * i)] is set

{(F * g),(F * i)} is non empty V53() V54() V55() set

{(F * g)} is non empty trivial V53() V54() V55() 1 -element set

{{(F * g),(F * i)},{(F * g)}} is non empty set

addreal . [(F * g),(F * i)] is complex ext-real real set

multreal . (F,g) is complex ext-real real Element of REAL

[F,g] is set

{F,g} is non empty V53() V54() V55() set

{{F,g},{F}} is non empty set

multreal . [F,g] is complex ext-real real set

addreal . ((multreal . (F,g)),(F * i)) is complex ext-real real Element of REAL

[(multreal . (F,g)),(F * i)] is set

{(multreal . (F,g)),(F * i)} is non empty V53() V54() V55() set

{(multreal . (F,g))} is non empty trivial V53() V54() V55() 1 -element set

{{(multreal . (F,g)),(F * i)},{(multreal . (F,g))}} is non empty set

addreal . [(multreal . (F,g)),(F * i)] is complex ext-real real set

multreal . (F,i) is complex ext-real real Element of REAL

[F,i] is set

{F,i} is non empty V53() V54() V55() set

{{F,i},{F}} is non empty set

multreal . [F,i] is complex ext-real real set

addreal . ((multreal . (F,g)),(multreal . (F,i))) is complex ext-real real Element of REAL

[(multreal . (F,g)),(multreal . (F,i))] is set

{(multreal . (F,g)),(multreal . (F,i))} is non empty V53() V54() V55() set

{{(multreal . (F,g)),(multreal . (F,i))},{(multreal . (F,g))}} is non empty set

addreal . [(multreal . (F,g)),(multreal . (F,i))] is complex ext-real real set

addreal . (F,g) is complex ext-real real Element of REAL

addreal . [F,g] is complex ext-real real set

multreal . ((addreal . (F,g)),i) is complex ext-real real Element of REAL

[(addreal . (F,g)),i] is set

{(addreal . (F,g)),i} is non empty V53() V54() V55() set

{(addreal . (F,g))} is non empty trivial V53() V54() V55() 1 -element set

{{(addreal . (F,g)),i},{(addreal . (F,g))}} is non empty set

multreal . [(addreal . (F,g)),i] is complex ext-real real set

F + g is complex ext-real real Element of REAL

multreal . ((F + g),i) is complex ext-real real Element of REAL

[(F + g),i] is set

{(F + g),i} is non empty V53() V54() V55() set

{(F + g)} is non empty trivial V53() V54() V55() 1 -element set

{{(F + g),i},{(F + g)}} is non empty set

multreal . [(F + g),i] is complex ext-real real set

(F + g) * i is complex ext-real real Element of REAL

g * i is complex ext-real real Element of REAL

(F * i) + (g * i) is complex ext-real real Element of REAL

addreal . ((F * i),(g * i)) is complex ext-real real Element of REAL

[(F * i),(g * i)] is set

{(F * i),(g * i)} is non empty V53() V54() V55() set

{(F * i)} is non empty trivial V53() V54() V55() 1 -element set

{{(F * i),(g * i)},{(F * i)}} is non empty set

addreal . [(F * i),(g * i)] is complex ext-real real set

addreal . ((multreal . (F,i)),(g * i)) is complex ext-real real Element of REAL

[(multreal . (F,i)),(g * i)] is set

{(multreal . (F,i)),(g * i)} is non empty V53() V54() V55() set

{(multreal . (F,i))} is non empty trivial V53() V54() V55() 1 -element set

{{(multreal . (F,i)),(g * i)},{(multreal . (F,i))}} is non empty set

addreal . [(multreal . (F,i)),(g * i)] is complex ext-real real set

multreal . (g,i) is complex ext-real real Element of REAL

multreal . [g,i] is complex ext-real real set

addreal . ((multreal . (F,i)),(multreal . (g,i))) is complex ext-real real Element of REAL

[(multreal . (F,i)),(multreal . (g,i))] is set

{(multreal . (F,i)),(multreal . (g,i))} is non empty V53() V54() V55() set

{{(multreal . (F,i)),(multreal . (g,i))},{(multreal . (F,i))}} is non empty set

addreal . [(multreal . (F,i)),(multreal . (g,i))] is complex ext-real real set

F is complex ext-real real Element of REAL

() . F is complex ext-real real Element of REAL

g is complex ext-real real Element of REAL

multreal . (F,g) is complex ext-real real Element of REAL

[F,g] is set

{F,g} is non empty V53() V54() V55() set

{F} is non empty trivial V53() V54() V55() 1 -element set

{{F,g},{F}} is non empty set

multreal . [F,g] is complex ext-real real set

() . (multreal . (F,g)) is complex ext-real real Element of REAL

() . g is complex ext-real real Element of REAL

multreal . ((() . F),(() . g)) is complex ext-real real Element of REAL

[(() . F),(() . g)] is set

{(() . F),(() . g)} is non empty V53() V54() V55() set

{(() . F)} is non empty trivial V53() V54() V55() 1 -element set

{{(() . F),(() . g)},{(() . F)}} is non empty set

multreal . [(() . F),(() . g)] is complex ext-real real set

multreal . (F,g) is complex ext-real real Element of REAL

() . (multreal . (F,g)) is complex ext-real real Element of REAL

F * g is complex ext-real real Element of REAL

() . (F * g) is complex ext-real real Element of REAL

(F * g) ^2 is complex ext-real real Element of REAL

(F * g) * (F * g) is complex ext-real real set

F ^2 is complex ext-real real Element of REAL

F * F is complex ext-real real set

g ^2 is complex ext-real real Element of REAL

g * g is complex ext-real real set

(F ^2) * (g ^2) is complex ext-real real Element of REAL

multreal . ((F ^2),(g ^2)) is complex ext-real real Element of REAL

[(F ^2),(g ^2)] is set

{(F ^2),(g ^2)} is non empty V53() V54() V55() set

{(F ^2)} is non empty trivial V53() V54() V55() 1 -element set

{{(F ^2),(g ^2)},{(F ^2)}} is non empty set

multreal . [(F ^2),(g ^2)] is complex ext-real real set

() . F is complex ext-real real Element of REAL

multreal . ((() . F),(g ^2)) is complex ext-real real Element of REAL

[(() . F),(g ^2)] is set

{(() . F),(g ^2)} is non empty V53() V54() V55() set

{(() . F)} is non empty trivial V53() V54() V55() 1 -element set

{{(() . F),(g ^2)},{(() . F)}} is non empty set

multreal . [(() . F),(g ^2)] is complex ext-real real set

() . g is complex ext-real real Element of REAL

multreal . ((() . F),(() . g)) is complex ext-real real Element of REAL

[(() . F),(() . g)] is set

{(() . F),(() . g)} is non empty V53() V54() V55() set

{{(() . F),(() . g)},{(() . F)}} is non empty set

multreal . [(() . F),(() . g)] is complex ext-real real set

F is complex ext-real real set

multreal [;] (F,(id REAL)) is Relation-like Function-like set

g is complex ext-real real Element of REAL

multreal [;] (g,(id REAL)) is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

F is complex ext-real real set

multreal [;] (F,(id REAL)) is Relation-like Function-like set

g is complex ext-real real set

(multreal [;] (F,(id REAL))) . g is set

F * g is complex ext-real real Element of REAL

i is complex ext-real real Element of REAL

j is complex ext-real real Element of REAL

(id REAL) . j is complex ext-real real Element of REAL

multreal . (i,((id REAL) . j)) is complex ext-real real Element of REAL

[i,((id REAL) . j)] is set

{i,((id REAL) . j)} is non empty V53() V54() V55() set

{i} is non empty trivial V53() V54() V55() 1 -element set

{{i,((id REAL) . j)},{i}} is non empty set

multreal . [i,((id REAL) . j)] is complex ext-real real set

multreal . (i,j) is complex ext-real real Element of REAL

[i,j] is set

{i,j} is non empty V53() V54() V55() set

{{i,j},{i}} is non empty set

multreal . [i,j] is complex ext-real real set

F is complex ext-real real set

(F) is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

multreal [;] (F,(id REAL)) is Relation-like Function-like set

g is complex ext-real real set

(F) . g is complex ext-real real Element of REAL

F * g is complex ext-real real Element of REAL

F is complex ext-real real set

(F) is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

multreal [;] (F,(id REAL)) is Relation-like Function-like set

F is complex ext-real real Element of REAL

compreal . F is complex ext-real real Element of REAL

addreal . (F,(compreal . F)) is complex ext-real real Element of REAL

[F,(compreal . F)] is set

{F,(compreal . F)} is non empty V53() V54() V55() set

{F} is non empty trivial V53() V54() V55() 1 -element set

{{F,(compreal . F)},{F}} is non empty set

addreal . [F,(compreal . F)] is complex ext-real real set

addreal . ((compreal . F),F) is complex ext-real real Element of REAL

[(compreal . F),F] is set

{(compreal . F),F} is non empty V53() V54() V55() set

{(compreal . F)} is non empty trivial V53() V54() V55() 1 -element set

{{(compreal . F),F},{(compreal . F)}} is non empty set

addreal . [(compreal . F),F] is complex ext-real real set

compreal . F is complex ext-real real Element of REAL

addreal . (F,(compreal . F)) is complex ext-real real Element of REAL

[F,(compreal . F)] is set

{F,(compreal . F)} is non empty V53() V54() V55() set

{{F,(compreal . F)},{F}} is non empty set

addreal . [F,(compreal . F)] is complex ext-real real set

F + (compreal . F) is complex ext-real real Element of REAL

- F is complex ext-real real Element of REAL

F + (- F) is complex ext-real real Element of REAL

addreal . ((compreal . F),F) is complex ext-real real Element of REAL

[(compreal . F),F] is set

{(compreal . F),F} is non empty V53() V54() V55() set

{(compreal . F)} is non empty trivial V53() V54() V55() 1 -element set

{{(compreal . F),F},{(compreal . F)}} is non empty set

addreal . [(compreal . F),F] is complex ext-real real set

(compreal . F) + F is complex ext-real real Element of REAL

(- F) + F is complex ext-real real Element of REAL

the_inverseOp_wrt addreal is Relation-like Function-like non empty V14( REAL ) V18( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

(F) is V53() V54() V55() Element of bool REAL

F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

F + g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

addreal .: (F,g) is Relation-like Function-like set

q2 is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

dom addreal is set

i is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

(i) is V53() V54() V55() Element of bool REAL

j is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

(j) is V53() V54() V55() Element of bool REAL

[:(i),(j):] is Relation-like complex-valued ext-real-valued real-valued set

dom (addreal .: (F,g)) is set

dom F is V53() V54() V55() V56() V57() V58() Element of bool NAT

dom g is V53() V54() V55() V56() V57() V58() Element of bool NAT

(dom F) /\ (dom g) is V53() V54() V55() V56() V57() V58() set

dom (F + g) is V53() V54() V55() V56() V57() V58() Element of bool NAT

p3 is set

q2 . p3 is complex ext-real real Element of REAL

F . p3 is complex ext-real real Element of REAL

g . p3 is complex ext-real real Element of REAL

addreal . ((F . p3),(g . p3)) is complex ext-real real Element of REAL

[(F . p3),(g . p3)] is set

{(F . p3),(g . p3)} is non empty V53() V54() V55() set

{(F . p3)} is non empty trivial V53() V54() V55() 1 -element set

{{(F . p3),(g . p3)},{(F . p3)}} is non empty set

addreal . [(F . p3),(g . p3)] is complex ext-real real set

(F . p3) + (g . p3) is complex ext-real real Element of REAL

p3 is set

dom q2 is V53() V54() V55() V56() V57() V58() Element of bool NAT

q2 . p3 is complex ext-real real Element of REAL

F . p3 is complex ext-real real Element of REAL

g . p3 is complex ext-real real Element of REAL

addreal . ((F . p3),(g . p3)) is complex ext-real real Element of REAL

[(F . p3),(g . p3)] is set

{(F . p3),(g . p3)} is non empty V53() V54() V55() set

{(F . p3)} is non empty trivial V53() V54() V55() 1 -element set

{{(F . p3),(g . p3)},{(F . p3)}} is non empty set

addreal . [(F . p3),(g . p3)] is complex ext-real real set

(F . p3) + (g . p3) is complex ext-real real Element of REAL

i is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

j is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

q2 is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

addreal .: (j,q2) is Relation-like Function-like set

addreal .: (q2,j) is Relation-like Function-like set

dom addreal is set

f3 is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

(f3) is V53() V54() V55() Element of bool REAL

p3 is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

(p3) is V53() V54() V55() Element of bool REAL

[:(f3),(p3):] is Relation-like complex-valued ext-real-valued real-valued set

[:(p3),(f3):] is Relation-like complex-valued ext-real-valued real-valued set

addreal .: (p3,f3) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

dom (addreal .: (p3,f3)) is V53() V54() V55() V56() V57() V58() Element of bool NAT

dom p3 is V53() V54() V55() V56() V57() V58() Element of bool NAT

dom f3 is V53() V54() V55() V56() V57() V58() Element of bool NAT

(dom p3) /\ (dom f3) is V53() V54() V55() V56() V57() V58() set

addreal .: (f3,p3) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

dom (addreal .: (f3,p3)) is V53() V54() V55() V56() V57() V58() Element of bool NAT

a is set

i . a is complex ext-real real Element of REAL

f3 . a is complex ext-real real Element of REAL

p3 . a is complex ext-real real Element of REAL

addreal . ((f3 . a),(p3 . a)) is complex ext-real real Element of REAL

[(f3 . a),(p3 . a)] is set

{(f3 . a),(p3 . a)} is non empty V53() V54() V55() set

{(f3 . a)} is non empty trivial V53() V54() V55() 1 -element set

{{(f3 . a),(p3 . a)},{(f3 . a)}} is non empty set

addreal . [(f3 . a),(p3 . a)] is complex ext-real real set

addreal . ((p3 . a),(f3 . a)) is complex ext-real real Element of REAL

[(p3 . a),(f3 . a)] is set

{(p3 . a),(f3 . a)} is non empty V53() V54() V55() set

{(p3 . a)} is non empty trivial V53() V54() V55() 1 -element set

{{(p3 . a),(f3 . a)},{(p3 . a)}} is non empty set

addreal . [(p3 . a),(f3 . a)] is complex ext-real real set

(p3 . a) + (f3 . a) is complex ext-real real Element of REAL

F is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V60() cardinal set

F -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL

REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL

{ b

g is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL

i is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL

g + i is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

addreal .: (g,i) is Relation-like Function-like set

F is set

g is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V60() cardinal set

g -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL

{ b

i is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() g -element FinSequence-like FinSubsequence-like Element of g -tuples_on REAL

i . F is complex ext-real real Element of REAL

j is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() g -element FinSequence-like FinSubsequence-like Element of g -tuples_on REAL

(g,i,j) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() g -element FinSequence-like FinSubsequence-like Element of g -tuples_on REAL

addreal .: (i,j) is Relation-like Function-like set

(g,i,j) . F is complex ext-real real Element of REAL

j . F is complex ext-real real Element of REAL

(i . F) + (j . F) is complex ext-real real Element of REAL

Seg g is V53() V54() V55() V56() V57() V58() V60() g -element Element of bool NAT

{ b

dom j is V53() V54() V55() V56() V57() V58() g -element Element of bool NAT

dom i is V53() V54() V55() V56() V57() V58() g -element Element of bool NAT

dom (g,i,j) is V53() V54() V55() V56() V57() V58() g -element Element of bool NAT

0 + 0 is Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V41() V42() complex-valued ext-real-valued real-valued natural-valued V53() V54() V55() V56() V57() V58() V59() V60() Function-yielding V70() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

(i . F) + 0 is complex ext-real real Element of REAL

Seg g is V53() V54() V55() V56() V57() V58() V60() g -element Element of bool NAT

{ b

dom (g,i,j) is V53() V54() V55() V56() V57() V58() g -element Element of bool NAT

Seg g is V53() V54() V55() V56() V57() V58() V60() g -element Element of bool NAT

{ b

<*> REAL is Relation-like non-zero empty-yielding NAT -defined REAL -valued RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V41() complex-valued ext-real-valued real-valued natural-valued V53() V54() V55() V56() V57() V58() V59() V60() Function-yielding V70() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of REAL

F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

((<*> REAL),F) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

addreal .: ((<*> REAL),F) is Relation-like Function-like set

F is complex ext-real real set

<*F*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,F] is set

{1,F} is non empty V53() V54() V55() set

{{1,F},{1}} is non empty set

{[1,F]} is Relation-like Function-like constant non empty trivial 1 -element set

g is complex ext-real real set

<*g*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like set

[1,g] is set

{1,g} is non empty V53() V54() V55() set

{{1,g},{1}} is non empty set

{[1,g]} is Relation-like Function-like constant non empty trivial 1 -element set

(<*F*>,<*g*>) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

addreal .: (<*F*>,<*g*>) is Relation-like Function-like set

F + g is complex ext-real real Element of REAL

<*(F + g)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL

[1,(F + g)] is set

{1,(F + g)} is non empty V53() V54() V55() set

{{1,(F + g)},{1}} is non empty set

{[1,(F + g)]} is Relation-like Function-like constant non empty trivial 1 -element set

i is complex ext-real real Element of REAL

<*i*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL

[1,i] is set

{1,i} is non empty V53() V54() V55() set

{{1,i},{1}} is non empty set

{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set

j is complex ext-real real Element of REAL

<*j*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL

[1,j] is set

{1,j} is non empty V53() V54() V55() set

{{1,j},{1}} is non empty set

{[1,j]} is Relation-like Function-like constant non empty trivial 1 -element set

(<*i*>,<*j*>) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

addreal .: (<*i*>,<*j*>) is Relation-like Function-like set

addreal . (i,j) is complex ext-real real Element of REAL

[i,j] is set

{i,j} is non empty V53() V54() V55() set

{i} is non empty trivial V53() V54() V55() 1 -element set

{{i,j},{i}} is non empty set

addreal . [i,j] is complex ext-real real set

<*(addreal . (i,j))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued V47() decreasing non-decreasing non-increasing V60() 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL

[1,(addreal . (i,j))] is set

{1,(addreal . (i,j))} is non empty V53() V54() V55() set

{{1,(addreal . (i,j))},{1}} is non empty set

{[1,(addreal . (i,j))]} is Relation-like Function-like constant non empty trivial 1 -element set

F is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V60() cardinal set

g is complex ext-real real set

F |-> g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like set

Seg F is V53() V54() V55() V56() V57() V58() V60() F -element Element of bool NAT

{ b

(Seg F) --> g is Relation-like Seg F -defined Seg F -defined Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{g}) complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{g}:]

{g} is non empty trivial V53() V54() V55() 1 -element set

[:(Seg F),{g}:] is Relation-like complex-valued ext-real-valued real-valued set

bool [:(Seg F),{g}:] is set

i is complex ext-real real set

F |-> i is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like set

(Seg F) --> i is Relation-like Seg F -defined Seg F -defined Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{i}) complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{i}:]

{i} is non empty trivial V53() V54() V55() 1 -element set

[:(Seg F),{i}:] is Relation-like complex-valued ext-real-valued real-valued set

bool [:(Seg F),{i}:] is set

((F |-> g),(F |-> i)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

addreal .: ((F |-> g),(F |-> i)) is Relation-like Function-like set

g + i is complex ext-real real Element of REAL

F |-> (g + i) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL

F -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL

{ b

(Seg F) --> (g + i) is Relation-like Seg F -defined Seg F -defined REAL -valued Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{(g + i)}) complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{(g + i)}:]

{(g + i)} is non empty trivial V53() V54() V55() 1 -element set

[:(Seg F),{(g + i)}:] is Relation-like complex-valued ext-real-valued real-valued set

bool [:(Seg F),{(g + i)}:] is set

j is complex ext-real real Element of REAL

F |-> j is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL

(Seg F) --> j is Relation-like Seg F -defined Seg F -defined REAL -valued Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{j}) complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{j}:]

{j} is non empty trivial V53() V54() V55() 1 -element set

[:(Seg F),{j}:] is Relation-like complex-valued ext-real-valued real-valued set

bool [:(Seg F),{j}:] is set

q2 is complex ext-real real Element of REAL

F |-> q2 is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL

(Seg F) --> q2 is Relation-like Seg F -defined Seg F -defined REAL -valued Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{q2}) complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{q2}:]

{q2} is non empty trivial V53() V54() V55() 1 -element set

[:(Seg F),{q2}:] is Relation-like complex-valued ext-real-valued real-valued set

bool [:(Seg F),{q2}:] is set

(F,(F |-> j),(F |-> q2)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL

addreal .: ((F |-> j),(F |-> q2)) is Relation-like Function-like set

addreal . (j,q2) is complex ext-real real Element of REAL

[j,q2] is set

{j,q2} is non empty V53() V54() V55() set

{{j,q2},{j}} is non empty set

addreal . [j,q2] is complex ext-real real set

F |-> (addreal . (j,q2)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL

(Seg F) --> (addreal . (j,q2)) is Relation-like Seg F -defined Seg F -defined REAL -valued Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{(addreal . (j,q2))}) complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{(addreal . (j,q2))}:]

{(addreal . (j,q2))} is non empty trivial V53() V54() V55() 1 -element set

[:(Seg F),{(addreal . (j,q2))}:] is Relation-like complex-valued ext-real-valued real-valued set

bool [:(Seg F),{(addreal . (j,q2))}:] is set

F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

i is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

(g,i) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

addreal .: (g,i) is Relation-like Function-like set

(F,(g,i)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

addreal .: (F,(g,i)) is Relation-like Function-like set

(F,g) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

addreal .: (F,g) is Relation-like Function-like set

((F,g),i) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like FinSequence of REAL

addreal .: ((F,g),i) is Relation-like Function-like set

F is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real V41() V60() cardinal set

F -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL

{ b

g is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL

F |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL

Seg F is V53() V54() V55() V56() V57() V58() V60() F -element Element of bool NAT

{ b

(Seg F) --> 0 is Relation-like Seg F -defined Seg F -defined NAT -valued RAT -valued INT -valued Function-like constant V14( Seg F) V14( Seg F) V18( Seg F,{0}) complex-valued ext-real-valued real-valued natural-valued V60() Function-yielding V70() FinSequence-like FinSubsequence-like Element of bool [:(Seg F),{0}:]

{0} is functional non empty trivial V53() V54() V55() V56() V57() V58() 1 -element set

[:(Seg F),{0}:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:(Seg F),{0}:] is set

(F,g,(F |-> 0)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V60() F -element FinSequence-like FinSubsequence-like Element of F -tuples_on REAL

addreal .: (g,(F |-> 0)) is Relation-like Function-like set

g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

- g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

- 1 is non empty complex ext-real non positive negative real V41() set

(- 1) (#) g is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

F is set

(- g) . F is complex ext-real real Element of REAL

g . F is complex ext-real real Element of REAL

- (g . F) is complex ext-real real Element of REAL

F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

- F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

- 1 is non empty complex ext-real non positive negative real V41() set

(- 1) (#) F is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set

F (#) compreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V60() FinSequence-like FinSubsequence-like set