:: QUATERNI semantic presentation

REAL is non empty V45() V46() V47() V51() V52() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() Element of bool REAL

bool REAL is non empty set

omega is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() set

RAT+ is set

{} is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set

RAT is non empty V45() V46() V47() V48() V51() V52() set

{ [b

1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

{ [b

{ [b

bool { [b

( { [b

bool RAT+ is non empty set

bool (bool RAT+) is non empty set

DEDEKIND_CUTS is Element of bool (bool RAT+)

REAL+ is set

COMPLEX is non empty V45() V51() V52() set

INT is non empty V45() V46() V47() V48() V49() V51() V52() set

{{}} is non empty V45() V46() V47() V48() V49() V50() set

[:{{}},REAL+:] is Relation-like set

REAL+ \/ [:{{}},REAL+:] is set

[{},{}] is set

{{},{}} is non empty V45() V46() V47() V48() V49() V50() set

{{{},{}},{{}}} is non empty set

{[{},{}]} is Relation-like non empty set

(REAL+ \/ [:{{}},REAL+:]) \ {[{},{}]} is Element of bool (REAL+ \/ [:{{}},REAL+:])

bool (REAL+ \/ [:{{}},REAL+:]) is non empty set

{{},1} is non empty V45() V46() V47() V48() V49() V50() set

Funcs ({{},1},REAL) is functional non empty FUNCTION_DOMAIN of {{},1}, REAL

{ b

(Funcs ({{},1},REAL)) \ { b

bool (Funcs ({{},1},REAL)) is non empty set

((Funcs ({{},1},REAL)) \ { b

2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

[:2,REAL:] is Relation-like non empty V33() V34() V35() set

bool [:2,REAL:] is non empty set

0 is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V43() V44() V45() V46() V47() V48() V49() V50() V51() Element of NAT

{0,1} is non empty V45() V46() V47() V48() V49() V50() set

{ b

( not b

( not b

( b

{RAT+} is non empty set

{ b

( not b

( not b

( b

( not b

( not b

( b

bool { b

( not b

( not b

( b

RAT+ \/ DEDEKIND_CUTS is set

{} is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of RAT+

{ { b

(RAT+ \/ DEDEKIND_CUTS) \ { { b

bool (RAT+ \/ DEDEKIND_CUTS) is non empty set

sqrt 0 is complex real ext-real Element of REAL

sqrt 1 is complex real ext-real Element of REAL

4 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

{{},1,2,3} is non empty set

Funcs (4,REAL) is functional non empty FUNCTION_DOMAIN of 4, REAL

{ b

(Funcs (4,REAL)) \ { b

bool (Funcs (4,REAL)) is non empty set

((Funcs (4,REAL)) \ { b

() is set

z is set

z2 is set

m3 is set

m4 is set

(z,z2) --> (m3,m4) is Relation-like Function-like set

m1 is set

m2 is set

n1 is set

n2 is set

(m1,m2) --> (n1,n2) is Relation-like Function-like set

((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set

z is set

z2 is set

m1 is set

m2 is set

m3 is set

m4 is set

n1 is set

n2 is set

(z,z2,m1,m2,m3,m4,n1,n2) is set

(z,z2) --> (m3,m4) is Relation-like Function-like set

(m1,m2) --> (n1,n2) is Relation-like Function-like set

((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set

z is set

z2 is set

m1 is set

m2 is set

{z,z2,m1,m2} is non empty set

m3 is set

m4 is set

n1 is set

n2 is set

(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set

(z,z2) --> (m3,m4) is Relation-like Function-like set

(m1,m2) --> (n1,n2) is Relation-like Function-like set

((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set

dom (z,z2,m1,m2,m3,m4,n1,n2) is set

dom ((z,z2) --> (m3,m4)) is set

{z,z2} is non empty set

dom ((m1,m2) --> (n1,n2)) is set

{m1,m2} is non empty set

(dom ((z,z2) --> (m3,m4))) \/ (dom ((m1,m2) --> (n1,n2))) is set

z is set

z2 is set

m1 is set

m2 is set

m3 is set

m4 is set

n1 is set

n2 is set

(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set

(z,z2) --> (m3,m4) is Relation-like Function-like set

(m1,m2) --> (n1,n2) is Relation-like Function-like set

((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set

rng (z,z2,m1,m2,m3,m4,n1,n2) is set

{m3,m4,n1,n2} is non empty set

rng ((z,z2) --> (m3,m4)) is set

{m3,m4} is non empty set

rng ((m1,m2) --> (n1,n2)) is set

{n1,n2} is non empty set

(rng ((z,z2) --> (m3,m4))) \/ (rng ((m1,m2) --> (n1,n2))) is set

{m3,m4} \/ {n1,n2} is non empty set

rng (((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2))) is set

z is set

z2 is set

m1 is set

m2 is set

m3 is set

m4 is set

n1 is set

n2 is set

(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set

(z,z2) --> (m3,m4) is Relation-like Function-like set

(m1,m2) --> (n1,n2) is Relation-like Function-like set

((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set

(z,z2,m1,m2,m3,m4,n1,n2) . z is set

(z,z2,m1,m2,m3,m4,n1,n2) . z2 is set

(z,z2,m1,m2,m3,m4,n1,n2) . m1 is set

(z,z2,m1,m2,m3,m4,n1,n2) . m2 is set

((z,z2) --> (m3,m4)) . z is set

((z,z2) --> (m3,m4)) . z2 is set

((m1,m2) --> (n1,n2)) . m1 is set

((m1,m2) --> (n1,n2)) . m2 is set

dom ((m1,m2) --> (n1,n2)) is set

{m1,m2} is non empty set

z is set

z2 is set

m1 is set

m2 is set

m3 is set

m4 is set

n1 is set

n2 is set

{m3,m4,n1,n2} is non empty set

(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set

(z,z2) --> (m3,m4) is Relation-like Function-like set

(m1,m2) --> (n1,n2) is Relation-like Function-like set

((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set

rng (z,z2,m1,m2,m3,m4,n1,n2) is set

n4 is set

dom (z,z2,m1,m2,m3,m4,n1,n2) is set

{z,z2,m1,m2} is non empty set

(z,z2,m1,m2,m3,m4,n1,n2) . z is set

(z,z2,m1,m2,m3,m4,n1,n2) . z2 is set

(z,z2,m1,m2,m3,m4,n1,n2) . m1 is set

(z,z2,m1,m2,m3,m4,n1,n2) . m2 is set

z is set

z2 is set

m1 is set

m2 is set

m3 is set

m4 is set

n1 is set

n2 is set

(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set

(z,z2) --> (m3,m4) is Relation-like Function-like set

(m1,m2) --> (n1,n2) is Relation-like Function-like set

((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set

rng (z,z2,m1,m2,m3,m4,n1,n2) is set

{m3,m4,n1,n2} is non empty set

z is set

z2 is set

m1 is set

m2 is set

{z,z2,m1,m2} is non empty set

m3 is set

m4 is set

z is non empty set

z2 is set

m1 is set

m2 is set

m3 is set

m4 is Element of z

n1 is Element of z

n2 is Element of z

n3 is Element of z

(z2,m1,m2,m3,m4,n1,n2,n3) is Relation-like Function-like set

(z2,m1) --> (m4,n1) is Relation-like Function-like set

(m2,m3) --> (n2,n3) is Relation-like Function-like set

((z2,m1) --> (m4,n1)) +* ((m2,m3) --> (n2,n3)) is Relation-like Function-like set

{z2,m1,m2,m3} is non empty set

[:{z2,m1,m2,m3},z:] is Relation-like non empty set

bool [:{z2,m1,m2,m3},z:] is non empty set

(z2,m1) --> (m4,n1) is Relation-like {z2,m1} -defined z -valued Function-like non empty V14({z2,m1}) quasi_total Element of bool [:{z2,m1},z:]

{z2,m1} is non empty set

[:{z2,m1},z:] is Relation-like non empty set

bool [:{z2,m1},z:] is non empty set

(m2,m3) --> (n2,n3) is Relation-like {m2,m3} -defined z -valued Function-like non empty V14({m2,m3}) quasi_total Element of bool [:{m2,m3},z:]

{m2,m3} is non empty set

[:{m2,m3},z:] is Relation-like non empty set

bool [:{m2,m3},z:] is non empty set

rng (z2,m1,m2,m3,m4,n1,n2,n3) is set

rng ((z2,m1) --> (m4,n1)) is non empty Element of bool z

bool z is non empty set

rng ((m2,m3) --> (n2,n3)) is non empty Element of bool z

(rng ((z2,m1) --> (m4,n1))) \/ (rng ((m2,m3) --> (n2,n3))) is non empty Element of bool z

dom (z2,m1,m2,m3,m4,n1,n2,n3) is set

(NAT,0,1,2,3,0,0,1,0) is Relation-like {0,1,2,3} -defined NAT -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() V36() Element of bool [:{0,1,2,3},NAT:]

{0,1,2,3} is non empty set

[:{0,1,2,3},NAT:] is Relation-like RAT -valued INT -valued non empty V33() V34() V35() V36() set

bool [:{0,1,2,3},NAT:] is non empty set

(0,1) --> (0,0) is Relation-like NAT -defined Function-like set

(2,3) --> (1,0) is Relation-like NAT -defined Function-like set

((0,1) --> (0,0)) +* ((2,3) --> (1,0)) is Relation-like NAT -defined Function-like set

(NAT,0,1,2,3,0,0,0,1) is Relation-like {0,1,2,3} -defined NAT -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() V36() Element of bool [:{0,1,2,3},NAT:]

(2,3) --> (0,1) is Relation-like NAT -defined Function-like set

((0,1) --> (0,0)) +* ((2,3) --> (0,1)) is Relation-like NAT -defined Function-like set

() is set

() is set

<i> is set

(0,1) --> (0,1) is Relation-like NAT -defined {0,1} -defined REAL -valued Function-like non empty V14({0,1}) quasi_total V33() V34() V35() Element of bool [:{0,1},REAL:]

[:{0,1},REAL:] is Relation-like non empty V33() V34() V35() set

bool [:{0,1},REAL:] is non empty set

[*0,1*] is complex Element of COMPLEX

z2 is Relation-like 4 -defined REAL -valued Function-like V14(4) quasi_total V33() V34() V35() Element of Funcs (4,REAL)

z2 . 2 is complex real ext-real Element of REAL

z2 . 3 is complex real ext-real Element of REAL

z2 is complex real ext-real Element of REAL

m1 is complex real ext-real Element of REAL

m2 is complex real ext-real Element of REAL

m3 is complex real ext-real Element of REAL

(REAL,0,1,2,3,z2,m1,m2,m3) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]

[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set

bool [:{0,1,2,3},REAL:] is non empty set

(0,1) --> (z2,m1) is Relation-like NAT -defined Function-like set

(2,3) --> (m2,m3) is Relation-like NAT -defined Function-like set

((0,1) --> (z2,m1)) +* ((2,3) --> (m2,m3)) is Relation-like NAT -defined Function-like set

z2 is Relation-like 4 -defined REAL -valued Function-like V14(4) quasi_total V33() V34() V35() Element of Funcs (4,REAL)

z2 . 2 is complex real ext-real Element of REAL

z2 . 3 is complex real ext-real Element of REAL

z2 is complex real ext-real Element of REAL

m1 is complex real ext-real Element of REAL

m2 is complex real ext-real Element of REAL

m3 is complex real ext-real Element of REAL

(REAL,0,1,2,3,z2,m1,m2,m3) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]

[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set

bool [:{0,1,2,3},REAL:] is non empty set

(0,1) --> (z2,m1) is Relation-like NAT -defined Function-like set

(2,3) --> (m2,m3) is Relation-like NAT -defined Function-like set

((0,1) --> (z2,m1)) +* ((2,3) --> (m2,m3)) is Relation-like NAT -defined Function-like set

z is Element of ()

m1 is complex real ext-real set

m2 is complex real ext-real set

z is complex real ext-real set

z2 is complex real ext-real set

(0,1,2,3,z,z2,m1,m2) is Relation-like Function-like set

(0,1) --> (z,z2) is Relation-like NAT -defined Function-like set

(2,3) --> (m1,m2) is Relation-like NAT -defined Function-like set

((0,1) --> (z,z2)) +* ((2,3) --> (m1,m2)) is Relation-like NAT -defined Function-like set

m3 is complex real ext-real Element of REAL

m4 is complex real ext-real Element of REAL

[*m3,m4*] is complex Element of COMPLEX

n4 is () Element of ()

m3 is complex real ext-real Element of REAL

m4 is complex real ext-real Element of REAL

n1 is complex real ext-real Element of REAL

n2 is complex real ext-real Element of REAL

(REAL,0,1,2,3,m3,m4,n1,n2) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]

[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set

bool [:{0,1,2,3},REAL:] is non empty set

(0,1) --> (m3,m4) is Relation-like NAT -defined Function-like set

(2,3) --> (n1,n2) is Relation-like NAT -defined Function-like set

((0,1) --> (m3,m4)) +* ((2,3) --> (n1,n2)) is Relation-like NAT -defined Function-like set

n4 is Relation-like 4 -defined REAL -valued Function-like V14(4) quasi_total V33() V34() V35() Element of Funcs (4,REAL)

n4 . 2 is complex real ext-real Element of REAL

n4 . 3 is complex real ext-real Element of REAL

n4 is () Element of ()

n1 is complex real ext-real Element of REAL

n2 is complex real ext-real Element of REAL

m3 is () Element of ()

[*n1,n2*] is complex Element of COMPLEX

n3 is complex real ext-real Element of REAL

n4 is complex real ext-real Element of REAL

m4 is () Element of ()

[*n3,n4*] is complex Element of COMPLEX

b1 is () Element of ()

b2 is () Element of ()

z is complex real ext-real Element of REAL

z2 is complex real ext-real Element of REAL

(z,z2,0,0) is () Element of ()

[*z,z2*] is complex Element of COMPLEX

m1 is complex real ext-real Element of REAL

m2 is complex real ext-real Element of REAL

[*m1,m2*] is complex Element of COMPLEX

z is set

z2 is set

m1 is set

m2 is set

{z,z2,m1,m2} is non empty set

m3 is set

m4 is set

n1 is set

n2 is set

(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set

(z,z2) --> (m3,m4) is Relation-like Function-like set

(m1,m2) --> (n1,n2) is Relation-like Function-like set

((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set

n3 is Relation-like Function-like set

dom n3 is set

n3 . z is set

n3 . z2 is set

n3 . m1 is set

n3 . m2 is set

dom ((z,z2) --> (m3,m4)) is set

{z,z2} is non empty set

dom ((m1,m2) --> (n1,n2)) is set

{m1,m2} is non empty set

(dom ((z,z2) --> (m3,m4))) \/ (dom ((m1,m2) --> (n1,n2))) is set

b2 is set

n3 . b2 is set

((m1,m2) --> (n1,n2)) . b2 is set

((z,z2) --> (m3,m4)) . b2 is set

z is () set

z2 is complex real ext-real Element of REAL

m1 is complex real ext-real Element of REAL

[*z2,m1*] is complex Element of COMPLEX

(z2,m1,0,0) is () Element of ()

z2 is Relation-like Function-like set

dom z2 is set

rng z2 is set

z2 . 0 is set

z2 . 1 is set

z2 . 2 is set

z2 . 3 is set

m1 is complex real ext-real Element of REAL

m2 is complex real ext-real Element of REAL

m3 is complex real ext-real Element of REAL

m4 is complex real ext-real Element of REAL

(REAL,0,1,2,3,m1,m2,m3,m4) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]

[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set

bool [:{0,1,2,3},REAL:] is non empty set

(0,1) --> (m1,m2) is Relation-like NAT -defined Function-like set

(2,3) --> (m3,m4) is Relation-like NAT -defined Function-like set

((0,1) --> (m1,m2)) +* ((2,3) --> (m3,m4)) is Relation-like NAT -defined Function-like set

(m1,m2,m3,m4) is () Element of ()

(REAL,0,1,2,3,m1,m2,m3,m4) . 2 is complex real ext-real Element of REAL

(REAL,0,1,2,3,m1,m2,m3,m4) . 3 is complex real ext-real Element of REAL

z is set

z2 is set

m1 is set

m2 is set

m3 is set

[z,m3] is set

{z,m3} is non empty set

{z} is non empty set

{{z,m3},{z}} is non empty set

m4 is set

[z2,m4] is set

{z2,m4} is non empty set

{z2} is non empty set

{{z2,m4},{z2}} is non empty set

n1 is set

[m1,n1] is set

{m1,n1} is non empty set

{m1} is non empty set

{{m1,n1},{m1}} is non empty set

n2 is set

(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set

(z,z2) --> (m3,m4) is Relation-like Function-like set

(m1,m2) --> (n1,n2) is Relation-like Function-like set

((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set

[m2,n2] is set

{m2,n2} is non empty set

{m2} is non empty set

{{m2,n2},{m2}} is non empty set

{[z,m3],[z2,m4],[m1,n1],[m2,n2]} is non empty set

dom ((z,z2) --> (m3,m4)) is set

{z,z2} is non empty set

dom ((m1,m2) --> (n1,n2)) is set

{m1,m2} is non empty set

((z,z2) --> (m3,m4)) \/ ((m1,m2) --> (n1,n2)) is Relation-like set

{[z,m3],[z2,m4]} is Relation-like non empty set

{[z,m3],[z2,m4]} \/ ((m1,m2) --> (n1,n2)) is Relation-like non empty set

{[m1,n1],[m2,n2]} is Relation-like non empty set

{[z,m3],[z2,m4]} \/ {[m1,n1],[m2,n2]} is Relation-like non empty set

z is set

z2 is set

[z,z2] is set

{z,z2} is non empty set

{z} is non empty set

{{z,z2},{z}} is non empty set

m1 is set

{m1} is non empty set

z is Element of bool RAT+

z2 is Element of RAT+

m1 is Element of RAT+

m1 + m1 is Element of RAT+

m2 is Element of RAT+

m2 + m2 is Element of RAT+

m3 is Element of RAT+

m3 + m3 is Element of RAT+

z2 + {} is Element of RAT+

z2 + z2 is Element of RAT+

m1 + {} is Element of RAT+

m2 + {} is Element of RAT+

z is complex real ext-real Element of REAL

z2 is complex real ext-real Element of REAL

m1 is complex real ext-real Element of REAL

m2 is complex real ext-real Element of REAL

(REAL,0,1,2,3,z,z2,m1,m2) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]

[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set

bool [:{0,1,2,3},REAL:] is non empty set

(0,1) --> (z,z2) is Relation-like NAT -defined Function-like set

(2,3) --> (m1,m2) is Relation-like NAT -defined Function-like set

((0,1) --> (z,z2)) +* ((2,3) --> (m1,m2)) is Relation-like NAT -defined Function-like set

[0,z] is set

{0,z} is non empty V45() V46() V47() set

{0} is non empty V45() V46() V47() V48() V49() V50() set

{{0,z},{0}} is non empty set

[1,z2] is set

{1,z2} is non empty V45() V46() V47() set

{1} is non empty V45() V46() V47() V48() V49() V50() set

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

[2,m1] is set

{2,m1} is non empty V45() V46() V47() set

{2} is non empty V45() V46() V47() V48() V49() V50() set

{{2,m1},{2}} is non empty set

[3,m2] is set

{3,m2} is non empty V45() V46() V47() set

{3} is non empty V45() V46() V47() V48() V49() V50() set

{{3,m2},{3}} is non empty set

{[0,z],[1,z2],[2,m1],[3,m2]} is non empty set

{ [b

m4 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

[m4,n1] is set

{m4,n1} is non empty V45() V46() V47() V48() V49() V50() set

{m4} is non empty V45() V46() V47() V48() V49() V50() set

{{m4,n1},{m4}} is non empty set

{{m4}} is non empty set

{ [b

{ [b

bool { [b

n1 is set

[0,n1] is set

{0,n1} is non empty set

{{0,n1},{0}} is non empty set

n2 is set

[1,n2] is set

{1,n2} is non empty set

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

n3 is set

[2,n3] is set

{2,n3} is non empty set

{{2,n3},{2}} is non empty set

n4 is set

[3,n4] is set

{3,n4} is non empty set

{{3,n4},{3}} is non empty set

{[0,n1],[1,n2],[2,n3],[3,n4]} is non empty set

b1 is Element of bool RAT+

b2 is Element of RAT+

b3 is Element of RAT+

b2 is Element of RAT+

b3 is Element of RAT+

b4 is Element of RAT+

a3 is Element of RAT+

a4 is Element of RAT+

{{}} is non empty V45() V46() V47() V48() V49() V50() set

[:{{}},REAL+:] is Relation-like set

n1 is set

n2 is set

[n1,n2] is set

{n1,n2} is non empty set

{n1} is non empty set

{{n1,n2},{n1}} is non empty set

{0,n2} is non empty set

{0,n2} is non empty set

z is complex real ext-real Element of REAL

z2 is complex real ext-real Element of REAL

m1 is complex real ext-real Element of REAL

m2 is complex real ext-real Element of REAL

(REAL,0,1,2,3,z,z2,m1,m2) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]

[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set

bool [:{0,1,2,3},REAL:] is non empty set

(0,1) --> (z,z2) is Relation-like NAT -defined Function-like set

(2,3) --> (m1,m2) is Relation-like NAT -defined Function-like set

((0,1) --> (z,z2)) +* ((2,3) --> (m1,m2)) is Relation-like NAT -defined Function-like set

Funcs ({0,1},REAL) is functional non empty FUNCTION_DOMAIN of {0,1}, REAL

dom (REAL,0,1,2,3,z,z2,m1,m2) is non empty Element of bool {0,1,2,3}

bool {0,1,2,3} is non empty set

{2,3} is non empty V45() V46() V47() V48() V49() V50() set

{0,1} \/ {2,3} is non empty V45() V46() V47() V48() V49() V50() set

{ b

(Funcs ({0,1},REAL)) \ { b

bool (Funcs ({0,1},REAL)) is non empty set

z is set

z2 is set

m1 is set

m2 is set

m3 is set

m4 is set

n1 is set

n2 is set

(z,z2,m1,m2,m3,m4,n1,n2) is Relation-like Function-like set

(z,z2) --> (m3,m4) is Relation-like Function-like set

(m1,m2) --> (n1,n2) is Relation-like Function-like set

((z,z2) --> (m3,m4)) +* ((m1,m2) --> (n1,n2)) is Relation-like Function-like set

n3 is set

n4 is set

b1 is set

b2 is set

(z,z2,m1,m2,n3,n4,b1,b2) is Relation-like Function-like set

(z,z2) --> (n3,n4) is Relation-like Function-like set

(m1,m2) --> (b1,b2) is Relation-like Function-like set

((z,z2) --> (n3,n4)) +* ((m1,m2) --> (b1,b2)) is Relation-like Function-like set

(z,z2,m1,m2,m3,m4,n1,n2) . z is set

(z,z2,m1,m2,m3,m4,n1,n2) . z2 is set

(z,z2,m1,m2,m3,m4,n1,n2) . m1 is set

(z,z2,m1,m2,m3,m4,n1,n2) . m2 is set

z is complex real ext-real Element of REAL

z2 is complex real ext-real Element of REAL

m1 is complex real ext-real Element of REAL

m2 is complex real ext-real Element of REAL

(z,z2,m1,m2) is () Element of ()

m3 is complex real ext-real Element of REAL

m4 is complex real ext-real Element of REAL

n1 is complex real ext-real Element of REAL

n2 is complex real ext-real Element of REAL

(m3,m4,n1,n2) is () Element of ()

[*z,z2*] is complex Element of COMPLEX

(REAL,0,1,2,3,m3,m4,n1,n2) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]

[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set

bool [:{0,1,2,3},REAL:] is non empty set

(0,1) --> (m3,m4) is Relation-like NAT -defined Function-like set

(2,3) --> (n1,n2) is Relation-like NAT -defined Function-like set

((0,1) --> (m3,m4)) +* ((2,3) --> (n1,n2)) is Relation-like NAT -defined Function-like set

[*m3,m4*] is complex Element of COMPLEX

(REAL,0,1,2,3,z,z2,m1,m2) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]

[:{0,1,2,3},REAL:] is Relation-like non empty V33() V34() V35() set

bool [:{0,1,2,3},REAL:] is non empty set

(0,1) --> (z,z2) is Relation-like NAT -defined Function-like set

(2,3) --> (m1,m2) is Relation-like NAT -defined Function-like set

((0,1) --> (z,z2)) +* ((2,3) --> (m1,m2)) is Relation-like NAT -defined Function-like set

[*m3,m4*] is complex Element of COMPLEX

(REAL,0,1,2,3,m3,m4,n1,n2) is Relation-like {0,1,2,3} -defined REAL -valued Function-like non empty V14({0,1,2,3}) quasi_total V33() V34() V35() Element of bool [:{0,1,2,3},REAL:]

(0,1) --> (m3,m4) is Relation-like NAT -defined Function-like set

(2,3) --> (n1,n2) is Relation-like NAT -defined Function-like set

((0,1) --> (m3,m4)) +* ((2,3) --> (n1,n2)) is Relation-like NAT -defined Function-like set

z is () set

m1 is complex real ext-real Element of REAL

m2 is complex real ext-real Element of REAL

m3 is complex real ext-real Element of REAL

m4 is complex real ext-real Element of REAL

(m1,m2,m3,m4) is () Element of ()

z2 is () set

n1 is complex real ext-real Element of REAL

n2 is complex real ext-real Element of REAL

n3 is complex real ext-real Element of REAL

n4 is complex real ext-real Element of REAL

(n1,n2,n3,n4) is () Element of ()

m1 + n1 is complex real ext-real Element of REAL

m2 + n2 is complex real ext-real Element of REAL

m3 + n3 is complex real ext-real Element of REAL

m4 + n4 is complex real ext-real Element of REAL

((m1 + n1),(m2 + n2),(m3 + n3),(m4 + n4)) is () Element of ()

b1 is set

b2 is set

b3 is complex real ext-real Element of REAL

b4 is complex real ext-real Element of REAL

a3 is complex real ext-real Element of REAL

a4 is complex real ext-real Element of REAL

(b3,b4,a3,a4) is () Element of ()

a5 is complex real ext-real Element of REAL

a6 is complex real ext-real Element of REAL

a7 is complex real ext-real Element of REAL

a8 is complex real ext-real Element of REAL

(a5,a6,a7,a8) is () Element of ()

b3 + a5 is complex real ext-real Element of REAL

b4 + a6 is complex real ext-real Element of REAL

a3 + a7 is complex real ext-real Element of REAL

a4 + a8 is complex real ext-real Element of REAL

((b3 + a5),(b4 + a6),(a3 + a7),(a4 + a8)) is () Element of ()

a9 is complex real ext-real Element of REAL

a10 is complex real ext-real Element of REAL

a11 is complex real ext-real Element of REAL

a12 is complex real ext-real Element of REAL

(a9,a10,a11,a12) is () Element of ()

b1 is complex real ext-real Element of REAL

b2 is complex real ext-real Element of REAL

b3 is complex real ext-real Element of REAL

b4 is complex real ext-real Element of REAL

(b1,b2,b3,b4) is () Element of ()

a9 + b1 is complex real ext-real Element of REAL

a10 + b2 is complex real ext-real Element of REAL

a11 + b3 is complex real ext-real Element of REAL

a12 + b4 is complex real ext-real Element of REAL

((a9 + b1),(a10 + b2),(a11 + b3),(a12 + b4)) is () Element of ()

b2 is () set

b4 is complex real ext-real Element of REAL

a3 is complex real ext-real Element of REAL

a4 is complex real ext-real Element of REAL

a5 is complex real ext-real Element of REAL

(b4,a3,a4,a5) is () Element of ()

b3 is () set

a6 is complex real ext-real Element of REAL

a7 is complex real ext-real Element of REAL

a8 is complex real ext-real Element of REAL

a9 is complex real ext-real Element of REAL

(a6,a7,a8,a9) is () Element of ()

b1 is set

b4 + a6 is complex real ext-real Element of REAL

a3 + a7 is complex real ext-real Element of REAL

a4 + a8 is complex real ext-real Element of REAL

a5 + a9 is complex real ext-real Element of REAL

((b4 + a6),(a3 + a7),(a4 + a8),(a5 + a9)) is () Element of ()

(0,0,0,0) is () Element of ()

z is complex real ext-real Element of REAL

z2 is complex real ext-real Element of REAL

[*z,z2*] is complex Element of COMPLEX

z is () set

z2 is complex real ext-real Element of REAL

m1 is complex real ext-real Element of REAL

m2 is complex real ext-real Element of REAL

m3 is complex real ext-real Element of REAL

(z2,m1,m2,m3) is () Element of ()

- z2 is complex real ext-real Element of REAL

- m1 is complex real ext-real Element of REAL

- m2 is complex real ext-real Element of REAL

- m3 is complex real ext-real Element of REAL

((- z2),(- m1),(- m2),(- m3)) is () Element of ()

m4 is () set

(z,m4) is set

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

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

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

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

m4 is () set

(z,m4) is set

n1 is () set

(z,n1) is set

n2 is complex real ext-real Element of REAL

n3 is complex real ext-real Element of REAL

n4 is complex real ext-real Element of REAL

b1 is complex real ext-real Element of REAL

(n2,n3,n4,b1) is () Element of ()

b2 is complex real ext-real Element of REAL

b3 is complex real ext-real Element of REAL

b4 is complex real ext-real Element of REAL

a3 is complex real ext-real Element of REAL

(b2,b3,b4,a3) is () Element of ()

n2 + b2 is complex real ext-real Element of REAL

n3 + b3 is complex real ext-real Element of REAL

n4 + b4 is complex real ext-real Element of REAL

b1 + a3 is complex real ext-real Element of REAL

((n2 + b2),(n3 + b3),(n4 + b4),(b1 + a3)) is () Element of ()

a4 is complex real ext-real Element of REAL

a5 is complex real ext-real Element of REAL

a6 is complex real ext-real Element of REAL

a7 is complex real ext-real Element of REAL

(a4,a5,a6,a7) is () Element of ()

a8 is complex real ext-real Element of REAL

a9 is complex real ext-real Element of REAL

a10 is complex real ext-real Element of REAL

a11 is complex real ext-real Element of REAL

(a8,a9,a10,a11) is () Element of ()

a4 + a8 is complex real ext-real Element of REAL

a5 + a9 is complex real ext-real Element of REAL

a6 + a10 is complex real ext-real Element of REAL

a7 + a11 is complex real ext-real Element of REAL

((a4 + a8),(a5 + a9),(a6 + a10),(a7 + a11)) is () Element of ()

n2 + a8 is complex real ext-real Element of REAL

n3 + a9 is complex real ext-real Element of REAL

n4 + a10 is complex real ext-real Element of REAL

b1 + a11 is complex real ext-real Element of REAL

n1 is () set

m4 is () set

(n1,m4) is set

(m4,n1) is set

z is () set

z2 is () set

(z2) is () set

(z,(z2)) is set

z is () set

m1 is complex real ext-real Element of REAL

m2 is complex real ext-real Element of REAL

m3 is complex real ext-real Element of REAL

m4 is complex real ext-real Element of REAL

(m1,m2,m3,m4) is () Element of ()

z2 is () set

n1 is complex real ext-real Element of REAL

n2 is complex real ext-real Element of REAL

n3 is complex real ext-real Element of REAL

n4 is complex real ext-real Element of REAL

(n1,n2,n3,n4) is () Element of ()

m1 * n1 is complex real ext-real Element of REAL

m2 * n2 is complex real ext-real Element of REAL

(m1 * n1) - (m2 * n2) is complex real ext-real Element of REAL

- (m2 * n2) is complex real ext-real set

(m1 * n1) + (- (m2 * n2)) is complex real ext-real set

m3 * n3 is complex real ext-real Element of REAL

((m1 * n1) - (m2 * n2)) - (m3 * n3) is complex real ext-real Element of REAL

- (m3 * n3) is complex real ext-real set

((m1 * n1) - (m2 * n2)) + (- (m3 * n3)) is complex real ext-real set

m4 * n4 is complex real ext-real Element of REAL

(((m1 * n1) - (m2 * n2)) - (m3 * n3)) - (m4 * n4) is complex real ext-real Element of REAL

- (m4 * n4) is complex real ext-real set

(((m1 * n1) - (m2 * n2)) - (m3 * n3)) + (- (m4 * n4)) is complex real ext-real set

m1 * n2 is complex real ext-real Element of REAL

m2 * n1 is complex real ext-real Element of REAL

(m1 * n2) + (m2 * n1) is complex real ext-real Element of REAL

m3 * n4 is complex real ext-real Element of REAL

((m1 * n2) + (m2 * n1)) + (m3 * n4) is complex real ext-real Element of REAL

m4 * n3 is complex real ext-real Element of REAL

(((m1 * n2) + (m2 * n1)) + (m3 * n4)) - (m4 * n3) is complex real ext-real Element of REAL

- (m4 * n3) is complex real ext-real set

(((m1 * n2) + (m2 * n1)) + (m3 * n4)) + (- (m4 * n3)) is complex real ext-real set

m1 * n3 is complex real ext-real Element of REAL

n1 * m3 is complex real ext-real Element of REAL

(m1 * n3) + (n1 * m3) is complex real ext-real Element of REAL

n2 * m4 is complex real ext-real Element of REAL

((m1 * n3) + (n1 * m3)) + (n2 * m4) is complex real ext-real Element of REAL

n4 * m2 is complex real ext-real Element of REAL

(((m1 * n3) + (n1 * m3)) + (n2 * m4)) - (n4 * m2) is complex real ext-real Element of REAL

- (n4 * m2) is complex real ext-real set

(((m1 * n3) + (n1 * m3)) + (n2 * m4)) + (- (n4 * m2)) is complex real ext-real set

m1 * n4 is complex real ext-real Element of REAL

m4 * n1 is complex real ext-real Element of REAL

(m1 * n4) + (m4 * n1) is complex real ext-real Element of REAL

m2 * n3 is complex real ext-real Element of REAL

((m1 * n4) + (m4 * n1)) + (m2 * n3) is complex real ext-real Element of REAL

m3 * n2 is complex real ext-real Element of REAL

(((m1 * n4) + (m4 * n1)) + (m2 * n3)) - (m3 * n2) is complex real ext-real Element of REAL

- (m3 * n2) is complex real ext-real set

(((m1 * n4) + (m4 * n1)) + (m2 * n3)) + (- (m3 * n2)) is complex real ext-real set

(((((m1 * n1) - (m2 * n2)) - (m3 * n3)) - (m4 * n4)),((((m1 * n2) + (m2 * n1)) + (m3 * n4)) - (m4 * n3)),((((m1 * n3) + (n1 * m3)) + (n2 * m4)) - (n4 * m2)),((((m1 * n4) + (m4 * n1)) + (m2 * n3)) - (m3 * n2))) is () Element of ()

b1 is set

b2 is set

b3 is complex real ext-real Element of REAL

b4 is complex real ext-real Element of REAL

a3 is complex real ext-real Element of REAL

a4 is complex real ext-real Element of REAL

(b3,b4,a3,a4) is () Element of ()

a5 is complex real ext-real Element of REAL

a6 is complex real ext-real Element of REAL

a7 is complex real ext-real Element of REAL

a8 is complex real ext-real Element of REAL

(a5,a6,a7,a8) is () Element of ()

b3 * a5 is complex real ext-real Element of REAL

b4 * a6 is complex real ext-real Element of REAL

(b3 * a5) - (b4 * a6) is complex real ext-real Element of REAL

- (b4 * a6) is complex real ext-real set

(b3 * a5) + (- (b4 * a6)) is complex real ext-real set

a3 * a7 is complex real ext-real Element of REAL

((b3 * a5) - (b4 * a6)) - (a3 * a7) is complex real ext-real Element of REAL

- (a3 * a7) is complex real ext-real set

((b3 * a5) - (b4 * a6)) + (- (a3 * a7)) is complex real ext-real set

a4 * a8 is complex real ext-real Element of REAL

(((b3 * a5) - (b4 * a6)) - (a3 * a7)) - (a4 * a8) is complex real ext-real Element of REAL

- (a4 * a8) is complex real ext-real set

(((b3 * a5) - (b4 * a6)) - (a3 * a7)) + (- (a4 * a8)) is complex real ext-real set

b3 * a6 is complex real ext-real Element of REAL

b4 * a5 is complex real ext-real Element of REAL

(b3 * a6) + (b4 * a5) is complex real ext-real Element of REAL

a3 * a8 is complex real ext-real Element of REAL

((b3 * a6) + (b4 * a5)) + (a3 * a8) is complex real ext-real Element of REAL

a4 * a7 is complex real ext-real Element of REAL

(((b3 * a6) + (b4 * a5)) + (a3 * a8)) - (a4 * a7) is complex real ext-real Element of REAL

- (a4 * a7) is complex real ext-real set

(((b3 * a6) + (b4 * a5)) + (a3 * a8)) + (- (a4 * a7)) is complex real ext-real set

b3 * a7 is complex real ext-real Element of REAL

a5 * a3 is complex real ext-real Element of REAL

(b3 * a7) + (a5 * a3) is complex real ext-real Element of REAL

a6 * a4 is complex real ext-real Element of REAL

((b3 * a7) + (a5 * a3)) + (a6 * a4) is complex real ext-real Element of REAL

a8 * b4 is complex real ext-real Element of REAL

(((b3 * a7) + (a5 * a3)) + (a6 * a4)) - (a8 * b4) is complex real ext-real Element of REAL

- (a8 * b4) is complex real ext-real set

(((b3 * a7) + (a5 * a3)) + (a6 * a4)) + (- (a8 * b4)) is complex real ext-real set

b3 * a8 is complex real ext-real Element of REAL

a4 * a5 is complex real ext-real Element of REAL

(b3 * a8) + (a4 * a5) is complex real ext-real Element of REAL

b4 * a7 is complex real ext-real Element of REAL

((b3 * a8) + (a4 * a5)) + (b4 * a7) is complex real ext-real Element of REAL

a3 * a6 is complex real ext-real Element of REAL

(((b3 * a8) + (a4 * a5)) + (b4 * a7)) - (a3 * a6) is complex real ext-real Element of REAL

- (a3 * a6) is complex real ext-real set

(((b3 * a8) + (a4 * a5)) + (b4 * a7)) + (- (a3 * a6)) is complex real ext-real set

(((((b3 * a5) - (b4 * a6)) - (a3 * a7)) - (a4 * a8)),((((b3 * a6) + (b4 * a5)) + (a3 * a8)) - (a4 * a7)),((((b3 * a7) + (a5 * a3)) + (a6 * a4)) - (a8 * b4)),((((b3 * a8) + (a4 * a5)) + (b4 * a7)) - (a3 * a6))) is () Element of ()

a9 is complex real ext-real Element of REAL

a10 is complex real ext-real Element of REAL

a11 is complex real ext-real Element of REAL

a12 is complex real ext-real Element of REAL

(a9,a10,a11,a12) is () Element of ()

b1 is complex real ext-real Element of REAL

b2 is complex real ext-real Element of REAL

b3 is complex real ext-real Element of REAL

b4 is complex real ext-real Element of REAL

(b1,b2,b3,b4) is () Element of ()

a9 * b1 is complex real ext-real Element of REAL

a10 * b2 is complex real ext-real Element of REAL

(a9 * b1) - (a10 * b2) is complex real ext-real Element of REAL

- (a10 * b2) is complex real ext-real set

(a9 * b1) + (- (a10 * b2)) is complex real ext-real set

a11 * b3 is complex real ext-real Element of REAL

((a9 * b1) - (a10 * b2)) - (a11 * b3) is complex real ext-real Element of REAL

- (a11 * b3) is complex real ext-real set

((a9 * b1) - (a10 * b2)) + (- (a11 * b3)) is complex real ext-real set

a12 * b4 is complex real ext-real Element of REAL

(((a9 * b1) - (a10 * b2)) - (a11 * b3)) - (a12 * b4) is complex real ext-real Element of REAL

- (a12 * b4) is complex real ext-real set

(((a9 * b1) - (a10 * b2)) - (a11 * b3)) + (- (a12 * b4)) is complex real ext-real set

a9 * b2 is complex real ext-real Element of REAL

a10 * b1 is complex real ext-real Element of REAL

(a9 * b2) + (a10 * b1) is complex real ext-real Element of REAL

a11 * b4 is complex real ext-real Element of REAL

((a9 * b2) + (a10 * b1)) + (a11 * b4) is complex real ext-real Element of REAL

a12 * b3 is complex real ext-real Element of REAL

(((a9 * b2) + (a10 * b1)) + (a11 * b4)) - (a12 * b3) is complex real ext-real Element of REAL

- (a12 * b3) is complex real ext-real set

(((a9 * b2) + (a10 * b1)) + (a11 * b4)) + (- (a12 * b3)) is complex real ext-real set

a9 * b3 is complex real ext-real Element of REAL

b1 * a11 is complex real ext-real Element of REAL

(a9 * b3) + (b1 * a11) is complex real ext-real Element of REAL

b2 * a12 is complex real ext-real Element of REAL

((a9 * b3) + (b1 * a11)) + (b2 * a12) is complex real ext-real Element of REAL

b4 * a10 is complex real ext-real Element of REAL

(((a9 * b3) + (b1 * a11)) + (b2 * a12)) - (b4 * a10) is complex real ext-real Element of REAL

- (b4 * a10) is complex real ext-real set

(((a9 * b3) + (b1 * a11)) + (b2 * a12)) + (- (b4 * a10)) is complex real ext-real set

a9 * b4 is complex real ext-real Element of REAL

a12 * b1 is complex real ext-real Element of REAL

(a9 * b4) + (a12 * b1) is complex real ext-real Element of REAL

a10 * b3 is complex real ext-real Element of REAL

((a9 * b4) + (a12 * b1)) + (a10 * b3) is complex real ext-real Element of REAL

a11 * b2 is complex real ext-real Element of REAL

(((a9 * b4) + (a12 * b1)) + (a10 * b3)) - (a11 * b2) is complex real ext-real Element of REAL

- (a11 * b2) is complex real ext-real set

(((a9 * b4) + (a12 * b1)) + (a10 * b3)) + (- (a11 * b2)) is complex real ext-real set

(((((a9 * b1) - (a10 * b2)) - (a11 * b3)) - (a12 * b4)),((((a9 * b2) + (a10 * b1)) + (a11 * b4)) - (a12 * b3)),((((a9 * b3) + (b1 * a11)) + (b2 * a12)) - (b4 * a10)),((((a9 * b4) + (a12 * b1)) + (a10 * b3)) - (a11 * b2))) is () Element of ()

z is () set

z2 is () set

(z,z2) is set

m1 is complex real ext-real Element of REAL

m2 is complex real ext-real Element of REAL

m3 is complex real ext-real Element of REAL

m4 is complex real ext-real Element of REAL

(m1,m2,m3,m4) is () Element of ()

n1 is complex real ext-real Element of REAL

n2 is complex real ext-real Element of REAL

n3 is complex real ext-real Element of REAL

n4 is complex real ext-real Element of REAL

(n1,n2,n3,n4) is () Element of ()

m1 + n1 is complex real ext-real Element of REAL

m2 + n2 is complex real ext-real Element of REAL

m3 + n3 is complex real ext-real Element of REAL

m4 + n4 is complex real ext-real Element of REAL

((m1 + n1),(m2 + n2),(m3 + n3),(m4 + n4)) is () Element of ()

(z,z2) is set

m1 is complex real ext-real Element of REAL

m2 is complex real ext-real Element of REAL

m3 is complex real ext-real Element of REAL

m4 is complex real ext-real Element of REAL

(m1,m2,m3,m4) is () Element of ()

n1 is complex real ext-real Element of REAL

n2 is complex real ext-real Element of REAL

n3 is complex real ext-real Element of REAL

n4 is complex real ext-real Element of REAL

(n1,n2,n3,n4) is () Element of ()

m1 * n1 is complex real ext-real Element of REAL

m2 * n2 is complex real ext-real Element of REAL

(m1 * n1) - (m2 * n2) is complex real ext-real Element of REAL

- (m2 * n2) is complex real ext-real set

(m1 * n1) + (- (m2 * n2)) is complex real ext-real set

m3 * n3 is complex real ext-real Element of REAL

((m1 * n1) - (m2 * n2)) - (m3 * n3) is complex real ext-real Element of REAL

- (m3 * n3) is complex real ext-real set

((m1 * n1) - (m2 * n2)) + (- (m3 * n3)) is complex real ext-real set

m4 * n4 is complex real ext-real Element of REAL

(((m1 * n1) - (m2 * n2)) - (m3 * n3)) - (m4 * n4) is complex real ext-real Element of REAL

- (m4 * n4) is complex real ext-real set

(((m1 * n1) - (m2 * n2)) - (m3 * n3)) + (- (m4 * n4)) is complex real ext-real set

m1 * n2 is complex real ext-real Element of REAL

m2 * n1 is complex real ext-real Element of REAL

(m1 * n2) + (m2 * n1) is complex real ext-real Element of REAL

m3 * n4 is complex real ext-real Element of REAL

((m1 * n2) + (m2 * n1)) + (m3 * n4) is complex real ext-real Element of REAL

m4 * n3 is complex real ext-real Element of REAL

(((m1 * n2) + (m2 * n1)) + (m3 * n4)) - (m4 * n3) is complex real ext-real Element of REAL

- (m4 * n3) is complex real ext-real set

(((m1 * n2) + (m2 * n1)) + (m3 * n4)) + (- (m4 * n3)) is complex real ext-real set

m1 * n3 is complex real ext-real Element of REAL

n1 * m3 is complex real ext-real Element of REAL

(m1 * n3) + (n1 * m3) is complex real ext-real Element of REAL

n2 * m4 is complex real ext-real Element of REAL

((m1 * n3) + (n1 * m3)) + (n2 * m4) is complex real ext-real Element of REAL

n4 * m2 is complex real ext-real Element of REAL

(((m1 * n3) + (n1 * m3)) + (n2 * m4)) - (n4 * m2) is complex real ext-real Element of REAL

- (n4 * m2) is complex real ext-real set

(((m1 * n3) + (n1 * m3)) + (n2 * m4)) + (- (n4 * m2)) is complex real ext-real set

m1 * n4 is complex real ext-real Element of REAL

m4 * n1 is complex real ext-real Element of REAL

(m1 * n4) + (m4 * n1) is complex real ext-real Element of REAL

m2 * n3 is complex real ext-real Element of REAL

((m1 * n4) + (m4 * n1)) + (m2 * n3) is complex real ext-real Element of REAL

m3 * n2 is complex real ext-real Element of REAL

(((m1 * n4) + (m4 * n1)) + (m2 * n3)) - (m3 * n2) is complex real ext-real Element of REAL

- (m3 * n2) is complex real ext-real set

(((m1 * n4) + (m4 * n1)) + (m2 * n3)) + (- (m3 * n2)) is complex real ext-real set

(((((m1 * n1) - (m2 * n2)) - (m3 * n3)) - (m4 * n4)),((((m1 * n2) + (m2 * n1)) + (m3 * n4)) - (m4 * n3)),((((m1 * n3) + (n1 * m3)) + (n2 * m4)) - (n4 * m2)),((((m1 * n4) + (m4 * n1)) + (m2 * n3)) - (m3 * n2))) is () Element of ()

(0,0,1,0) is () Element of ()

z is () Element of ()

z2 is () Element of ()

(0,0,0,1) is () Element of ()

z is () Element of ()

z2 is () Element of ()

() is () Element of ()

() is () Element of ()

(<i>,<i>) is () set

- 1 is complex real ext-real non positive Element of REAL

(0,1,0,0) is () Element of ()

0 * 0 is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

1 * 1 is complex real ext-real non negative Element of REAL

(0 * 0) - (1 * 1) is complex real ext-real non positive Element of REAL

- (1 * 1) is complex real ext-real non positive set

(0 * 0) + (- (1 * 1)) is complex real ext-real non positive set

((0 * 0) - (1 * 1)) - (0 * 0) is complex real ext-real non positive Element of REAL

- (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set

((0 * 0) - (1 * 1)) + (- (0 * 0)) is complex real ext-real non positive set

(((0 * 0) - (1 * 1)) - (0 * 0)) - (0 * 0) is complex real ext-real non positive Element of REAL

(((0 * 0) - (1 * 1)) - (0 * 0)) + (- (0 * 0)) is complex real ext-real non positive set

0 * 1 is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

1 * 0 is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

(0 * 1) + (1 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

((0 * 1) + (1 * 0)) + (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

(((0 * 1) + (1 * 0)) + (0 * 0)) - (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

(((0 * 1) + (1 * 0)) + (0 * 0)) + (- (0 * 0)) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set

(0 * 0) + (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

((0 * 0) + (0 * 0)) + (1 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

(((0 * 0) + (0 * 0)) + (1 * 0)) - (0 * 1) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

- (0 * 1) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set

(((0 * 0) + (0 * 0)) + (1 * 0)) + (- (0 * 1)) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set

(((((0 * 0) - (1 * 1)) - (0 * 0)) - (0 * 0)),((((0 * 1) + (1 * 0)) + (0 * 0)) - (0 * 0)),((((0 * 0) + (0 * 0)) + (1 * 0)) - (0 * 1)),((((0 * 0) + (0 * 0)) + (1 * 0)) - (0 * 1))) is () Element of ()

((- 1),0,0,0) is () Element of ()

[*(- 1),0*] is complex Element of COMPLEX

((),()) is () set

0 * 0 is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

(0 * 0) - (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

- (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set

(0 * 0) + (- (0 * 0)) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set

1 * 1 is complex real ext-real non negative Element of REAL

((0 * 0) - (0 * 0)) - (1 * 1) is complex real ext-real non positive Element of REAL

- (1 * 1) is complex real ext-real non positive set

((0 * 0) - (0 * 0)) + (- (1 * 1)) is complex real ext-real non positive set

(((0 * 0) - (0 * 0)) - (1 * 1)) - (0 * 0) is complex real ext-real non positive Element of REAL

(((0 * 0) - (0 * 0)) - (1 * 1)) + (- (0 * 0)) is complex real ext-real non positive set

(0 * 0) + (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

((0 * 0) + (0 * 0)) + (0 * 0) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

0 * 1 is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

(((0 * 0) + (0 * 0)) + (0 * 0)) - (0 * 1) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() Element of REAL

- (0 * 1) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set

(((0 * 0) + (0 * 0)) + (0 * 0)) + (- (0 * 1)) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() set

(0 * 1) + (0 * 1) is Relation-like non-empty empty-yielding RAT -valued empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non