:: XCMPLX_0 semantic presentation

REAL is non empty set
NAT is Element of bool REAL
bool REAL is set
omega is set
K99() is set
bool K99() is set
bool (bool K99()) is set
DEDEKIND_CUTS is Element of bool (bool K99())
REAL+ is set
COMPLEX is non empty set
K105() is Function-like functional empty trivial Element of K99()
0 is Function-like functional empty trivial Element of NAT
{0} is non empty trivial set
[:{0},REAL+:] is set
1 is non empty Element of NAT
{} is Function-like functional empty trivial set
{{}} is non empty trivial set
[:{{}},REAL+:] is set
REAL+ \/ [:{{}},REAL+:] is set
[{},{}] is non empty set
{[{},{}]} is Function-like non empty trivial set
(REAL+ \/ [:{{}},REAL+:]) \ {[{},{}]} is Element of bool (REAL+ \/ [:{{}},REAL+:])
bool (REAL+ \/ [:{{}},REAL+:]) is set
{{},1} is non empty set
Funcs ({{},1},REAL) is functional non empty FUNCTION_DOMAIN of {{},1}, REAL
{ b₁ where b₁ is V1() Function-like V14({{},1}) quasi_total Element of Funcs ({{},1},REAL) : b₁ . 1 = {} } is set
(Funcs ({{},1},REAL)) \ { b₁ where b₁ is V1() Function-like V14({{},1}) quasi_total Element of Funcs ({{},1},REAL) : b₁ . 1 = {} } is functional Element of bool (Funcs ({{},1},REAL))
bool (Funcs ({{},1},REAL)) is set
((Funcs ({{},1},REAL)) \ { b₁ where b₁ is V1() Function-like V14({{},1}) quasi_total Element of Funcs ({{},1},REAL) : b₁ . 1 = {} } ) \/ REAL is non empty set
(0,1) --> (0,1) is Function-like non empty V14({0,1}) quasi_total Element of bool [:{0,1},REAL:]
{0,1} is non empty set
[:{0,1},REAL:] is set
bool [:{0,1},REAL:] is set
() is set
Funcs ({0,1},REAL) is functional non empty FUNCTION_DOMAIN of {0,1}, REAL
{ b₁ where b₁ is V1() Function-like V14({0,1}) quasi_total Element of Funcs ({0,1},REAL) : b₁ . 1 = 0 } is set
n is V1() Function-like V14({0,1}) quasi_total Element of Funcs ({0,1},REAL)
n . 1 is set
(Funcs ({0,1},REAL)) \ { b₁ where b₁ is V1() Function-like V14({0,1}) quasi_total Element of Funcs ({0,1},REAL) : b₁ . 1 = 0 } is functional Element of bool (Funcs ({0,1},REAL))
bool (Funcs ({0,1},REAL)) is set
j is () set
j is () set
j is () set
y is Element of REAL
j is Element of REAL
[*y,j*] is Element of COMPLEX
n is () set
u1 is Element of REAL
u2 is Element of REAL
[*u1,u2*] is Element of COMPLEX
+ (y,u1) is Element of REAL
+ (j,u2) is Element of REAL
[*(+ (y,u1)),(+ (j,u2))*] is Element of COMPLEX
v1 is set
v2 is set
z is Element of REAL
u1 is Element of REAL
[*z,u1*] is Element of COMPLEX
u2 is Element of REAL
v1 is Element of REAL
[*u2,v1*] is Element of COMPLEX
+ (z,u2) is Element of REAL
+ (u1,v1) is Element of REAL
[*(+ (z,u2)),(+ (u1,v1))*] is Element of COMPLEX
v2 is Element of REAL
x4 is Element of REAL
[*v2,x4*] is Element of COMPLEX
yz1 is Element of REAL
yz2 is Element of REAL
[*yz1,yz2*] is Element of COMPLEX
+ (v2,yz1) is Element of REAL
+ (x4,yz2) is Element of REAL
[*(+ (v2,yz1)),(+ (x4,yz2))*] is Element of COMPLEX
v2 is () set
u1 is Element of REAL
u2 is Element of REAL
[*u1,u2*] is Element of COMPLEX
z is () set
v1 is Element of REAL
v2 is Element of REAL
[*v1,v2*] is Element of COMPLEX
v1 is set
+ (u1,v1) is Element of REAL
+ (u2,v2) is Element of REAL
[*(+ (u1,v1)),(+ (u2,v2))*] is Element of COMPLEX
* (y,u1) is Element of REAL
* (j,u2) is Element of REAL
opp (* (j,u2)) is Element of REAL
+ ((* (y,u1)),(opp (* (j,u2)))) is Element of REAL
* (y,u2) is Element of REAL
* (j,u1) is Element of REAL
+ ((* (y,u2)),(* (j,u1))) is Element of REAL
[*(+ ((* (y,u1)),(opp (* (j,u2))))),(+ ((* (y,u2)),(* (j,u1))))*] is Element of COMPLEX
v1 is set
v2 is set
z is Element of REAL
u1 is Element of REAL
[*z,u1*] is Element of COMPLEX
u2 is Element of REAL
v1 is Element of REAL
[*u2,v1*] is Element of COMPLEX
* (z,u2) is Element of REAL
* (u1,v1) is Element of REAL
opp (* (u1,v1)) is Element of REAL
+ ((* (z,u2)),(opp (* (u1,v1)))) is Element of REAL
* (z,v1) is Element of REAL
* (u1,u2) is Element of REAL
+ ((* (z,v1)),(* (u1,u2))) is Element of REAL
[*(+ ((* (z,u2)),(opp (* (u1,v1))))),(+ ((* (z,v1)),(* (u1,u2))))*] is Element of COMPLEX
v2 is Element of REAL
x4 is Element of REAL
[*v2,x4*] is Element of COMPLEX
yz1 is Element of REAL
yz2 is Element of REAL
[*yz1,yz2*] is Element of COMPLEX
* (v2,yz1) is Element of REAL
* (x4,yz2) is Element of REAL
opp (* (x4,yz2)) is Element of REAL
+ ((* (v2,yz1)),(opp (* (x4,yz2)))) is Element of REAL
* (v2,yz2) is Element of REAL
* (x4,yz1) is Element of REAL
+ ((* (v2,yz2)),(* (x4,yz1))) is Element of REAL
[*(+ ((* (v2,yz1)),(opp (* (x4,yz2))))),(+ ((* (v2,yz2)),(* (x4,yz1))))*] is Element of COMPLEX
v2 is () set
u1 is Element of REAL
u2 is Element of REAL
[*u1,u2*] is Element of COMPLEX
z is () set
v1 is Element of REAL
v2 is Element of REAL
[*v1,v2*] is Element of COMPLEX
v1 is set
* (u1,v1) is Element of REAL
* (u2,v2) is Element of REAL
opp (* (u2,v2)) is Element of REAL
+ ((* (u1,v1)),(opp (* (u2,v2)))) is Element of REAL
* (u1,v2) is Element of REAL
* (u2,v1) is Element of REAL
+ ((* (u1,v2)),(* (u2,v1))) is Element of REAL
[*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] is Element of COMPLEX
[*0,0*] is Element of COMPLEX
n is Element of REAL
y is Element of REAL
+ (n,y) is Element of REAL
j is Element of REAL
+ (n,j) is Element of REAL
u1 is Element of REAL+
u2 is Element of REAL+
u1 + u2 is Element of REAL+
v1 is Element of REAL+
v2 is Element of REAL+
v1 + v2 is Element of REAL+
u1 is Element of REAL+
u2 is Element of REAL+
[0,u2] is non empty set
u1 - u2 is set
v1 is Element of REAL+
v2 is Element of REAL+
v1 + v2 is Element of REAL+
u1 is Element of REAL+
u2 is Element of REAL+
[0,u2] is non empty set
u1 - u2 is set
v1 is Element of REAL+
v2 is Element of REAL+
v1 + v2 is Element of REAL+
[0,0] is non empty set
{[0,0]} is Function-like non empty trivial set
u1 is Element of REAL+
u2 is Element of REAL+
[0,u2] is non empty set
u1 - u2 is set
v1 is Element of REAL+
v2 is Element of REAL+
[0,v2] is non empty set
v1 - v2 is set
u1 is Element of REAL+
[0,u1] is non empty set
u2 is Element of REAL+
u2 - u1 is set
v1 is Element of REAL+
[0,v1] is non empty set
v2 is Element of REAL+
v2 - v1 is set
u1 is Element of REAL+
[0,u1] is non empty set
u2 is Element of REAL+
[0,u2] is non empty set
u1 + u2 is Element of REAL+
[0,(u1 + u2)] is non empty set
u1 is Element of REAL+
[0,u1] is non empty set
u2 is Element of REAL+
[0,u2] is non empty set
u1 + u2 is Element of REAL+
[0,(u1 + u2)] is non empty set
n is () set
y is () set
(n,y) is set
j is Element of REAL
u1 is Element of REAL
[*j,u1*] is Element of COMPLEX
u2 is Element of REAL
v1 is Element of REAL
[*u2,v1*] is Element of COMPLEX
+ (j,u2) is Element of REAL
+ (u1,v1) is Element of REAL
[*(+ (j,u2)),(+ (u1,v1))*] is Element of COMPLEX
(n,y) is set
j is Element of REAL
u1 is Element of REAL
[*j,u1*] is Element of COMPLEX
u2 is Element of REAL
v1 is Element of REAL
[*u2,v1*] is Element of COMPLEX
* (j,u2) is Element of REAL
* (u1,v1) is Element of REAL
opp (* (u1,v1)) is Element of REAL
+ ((* (j,u2)),(opp (* (u1,v1)))) is Element of REAL
* (j,v1) is Element of REAL
* (u1,u2) is Element of REAL
+ ((* (j,v1)),(* (u1,u2))) is Element of REAL
[*(+ ((* (j,u2)),(opp (* (u1,v1))))),(+ ((* (j,v1)),(* (u1,u2))))*] is Element of COMPLEX
n is () set
y is Element of REAL
j is Element of REAL
[*y,j*] is Element of COMPLEX
opp y is Element of REAL
opp j is Element of REAL
[*(opp y),(opp j)*] is Element of COMPLEX
u1 is () set
(n,u1) is () set
+ (y,(opp y)) is Element of REAL
+ (j,(opp j)) is Element of REAL
u1 is () set
(n,u1) is () set
u2 is () set
(n,u2) is () set
v1 is Element of REAL
v2 is Element of REAL
[*v1,v2*] is Element of COMPLEX
z is Element of REAL
u1 is Element of REAL
[*z,u1*] is Element of COMPLEX
+ (v1,z) is Element of REAL
+ (v2,u1) is Element of REAL
[*(+ (v1,z)),(+ (v2,u1))*] is Element of COMPLEX
u2 is Element of REAL
v1 is Element of REAL
[*u2,v1*] is Element of COMPLEX
v2 is Element of REAL
x4 is Element of REAL
[*v2,x4*] is Element of COMPLEX
+ (u2,v2) is Element of REAL
+ (v1,x4) is Element of REAL
[*(+ (u2,v2)),(+ (v1,x4))*] is Element of COMPLEX
+ (v1,v2) is Element of REAL
+ (v2,x4) is Element of REAL
u2 is () set
u1 is () set
(u2,u1) is () set
(u1,u2) is () set
* (y,y) is Element of REAL
* (j,j) is Element of REAL
+ ((* (y,y)),(* (j,j))) is Element of REAL
inv (+ ((* (y,y)),(* (j,j)))) is Element of REAL
* (y,(inv (+ ((* (y,y)),(* (j,j)))))) is Element of REAL
opp j is Element of REAL
* ((opp j),(inv (+ ((* (y,y)),(* (j,j)))))) is Element of REAL
[*(* (y,(inv (+ ((* (y,y)),(* (j,j))))))),(* ((opp j),(inv (+ ((* (y,y)),(* (j,j)))))))*] is Element of COMPLEX
v2 is () set
(n,v2) is () set
* (j,(* ((opp j),(inv (+ ((* (y,y)),(* (j,j)))))))) is Element of REAL
opp (* (j,(* ((opp j),(inv (+ ((* (y,y)),(* (j,j))))))))) is Element of REAL
* (j,(inv (+ ((* (y,y)),(* (j,j)))))) is Element of REAL
opp (* (j,(inv (+ ((* (y,y)),(* (j,j))))))) is Element of REAL
* (j,(opp (* (j,(inv (+ ((* (y,y)),(* (j,j))))))))) is Element of REAL
opp (* (j,(opp (* (j,(inv (+ ((* (y,y)),(* (j,j)))))))))) is Element of REAL
* (j,(* (j,(inv (+ ((* (y,y)),(* (j,j)))))))) is Element of REAL
opp (* (j,(* (j,(inv (+ ((* (y,y)),(* (j,j))))))))) is Element of REAL
opp (opp (* (j,(* (j,(inv (+ ((* (y,y)),(* (j,j)))))))))) is Element of REAL
* ((* (j,j)),(inv (+ ((* (y,y)),(* (j,j)))))) is Element of REAL
* (y,(* (y,(inv (+ ((* (y,y)),(* (j,j)))))))) is Element of REAL
* ((* (y,y)),(inv (+ ((* (y,y)),(* (j,j)))))) is Element of REAL
* (y,(* ((opp j),(inv (+ ((* (y,y)),(* (j,j)))))))) is Element of REAL
* ((opp j),(* (y,(inv (+ ((* (y,y)),(* (j,j)))))))) is Element of REAL
* (j,(* (y,(inv (+ ((* (y,y)),(* (j,j)))))))) is Element of REAL
opp (* (j,(* (y,(inv (+ ((* (y,y)),(* (j,j))))))))) is Element of REAL
+ ((* (y,(* ((opp j),(inv (+ ((* (y,y)),(* (j,j))))))))),(* (j,(* (y,(inv (+ ((* (y,y)),(* (j,j)))))))))) is Element of REAL
+ ((* (y,(* (y,(inv (+ ((* (y,y)),(* (j,j))))))))),(opp (* (j,(* ((opp j),(inv (+ ((* (y,y)),(* (j,j))))))))))) is Element of REAL
[*(+ ((* (y,(* (y,(inv (+ ((* (y,y)),(* (j,j))))))))),(opp (* (j,(* ((opp j),(inv (+ ((* (y,y)),(* (j,j)))))))))))),(+ ((* (y,(* ((opp j),(inv (+ ((* (y,y)),(* (j,j))))))))),(* (j,(* (y,(inv (+ ((* (y,y)),(* (j,j)))))))))))*] is Element of COMPLEX
* ((+ ((* (y,y)),(* (j,j)))),(inv (+ ((* (y,y)),(* (j,j)))))) is Element of REAL
u1 is () set
(n,u1) is () set
u2 is () set
(n,u2) is () set
* (y,y) is Element of REAL
* (j,j) is Element of REAL
+ ((* (y,y)),(* (j,j))) is Element of REAL
inv (+ ((* (y,y)),(* (j,j)))) is Element of REAL
* (y,(inv (+ ((* (y,y)),(* (j,j)))))) is Element of REAL
opp j is Element of REAL
* ((opp j),(inv (+ ((* (y,y)),(* (j,j)))))) is Element of REAL
[*(* (y,(inv (+ ((* (y,y)),(* (j,j))))))),(* ((opp j),(inv (+ ((* (y,y)),(* (j,j)))))))*] is Element of COMPLEX
v1 is () set
(n,v1) is () set
v2 is Element of REAL
z is Element of REAL
[*v2,z*] is Element of COMPLEX
u1 is Element of REAL
u2 is Element of REAL
[*u1,u2*] is Element of COMPLEX
* (v2,u1) is Element of REAL
* (z,u2) is Element of REAL
opp (* (z,u2)) is Element of REAL
+ ((* (v2,u1)),(opp (* (z,u2)))) is Element of REAL
* (v2,u2) is Element of REAL
* (z,u1) is Element of REAL
+ ((* (v2,u2)),(* (z,u1))) is Element of REAL
[*(+ ((* (v2,u1)),(opp (* (z,u2))))),(+ ((* (v2,u2)),(* (z,u1))))*] is Element of COMPLEX
+ (j,(opp j)) is Element of REAL
* (y,u2) is Element of REAL
* (y,u1) is Element of REAL
* (j,u2) is Element of REAL
opp (* (j,u2)) is Element of REAL
* (j,u1) is Element of REAL
+ (0,(* (j,u1))) is Element of REAL
[*(opp (* (j,u2))),(+ (0,(* (j,u1))))*] is Element of COMPLEX
[*(opp (* (j,u2))),(* (j,u1))*] is Element of COMPLEX
j is Element of REAL
[*j,0*] is Element of COMPLEX
* ((opp j),u2) is Element of REAL
inv (opp j) is Element of REAL
inv j is Element of REAL
opp (inv j) is Element of REAL
* ((opp j),(opp (inv j))) is Element of REAL
* (j,(opp (inv j))) is Element of REAL
opp (* (j,(opp (inv j)))) is Element of REAL
* (j,(inv j)) is Element of REAL
opp (* (j,(inv j))) is Element of REAL
opp (opp (* (j,(inv j)))) is Element of REAL
[*0,(inv (opp j))*] is Element of COMPLEX
* (j,(inv j)) is Element of REAL
opp (* (j,(inv j))) is Element of REAL
[*0,(opp (* (j,(inv j))))*] is Element of COMPLEX
* ((* (j,(inv j))),(inv j)) is Element of REAL
opp (* ((* (j,(inv j))),(inv j))) is Element of REAL
[*0,(opp (* ((* (j,(inv j))),(inv j))))*] is Element of COMPLEX
* ((inv j),(inv j)) is Element of REAL
* (j,(* ((inv j),(inv j)))) is Element of REAL
opp (* (j,(* ((inv j),(inv j))))) is Element of REAL
[*0,(opp (* (j,(* ((inv j),(inv j))))))*] is Element of COMPLEX
* ((opp j),(* ((inv j),(inv j)))) is Element of REAL
[*0,(* ((opp j),(* ((inv j),(inv j)))))*] is Element of COMPLEX
inv (* (j,j)) is Element of REAL
* ((opp j),(inv (* (j,j)))) is Element of REAL
[*0,(* ((opp j),(inv (* (j,j)))))*] is Element of COMPLEX
+ (0,(* (j,j))) is Element of REAL
inv (+ (0,(* (j,j)))) is Element of REAL
* ((opp j),(inv (+ (0,(* (j,j)))))) is Element of REAL
[*0,(* ((opp j),(inv (+ (0,(* (j,j)))))))*] is Element of COMPLEX
+ (j,(opp j)) is Element of REAL
* (j,u1) is Element of REAL
* (j,u2) is Element of REAL
opp (* (j,u2)) is Element of REAL
* ((opp j),u2) is Element of REAL
* (y,u1) is Element of REAL
* (y,u2) is Element of REAL
+ ((* (y,u2)),0) is Element of REAL
[*(* (y,u1)),(+ ((* (y,u2)),0))*] is Element of COMPLEX
[*(* (y,u1)),(* (y,u2))*] is Element of COMPLEX
j is Element of REAL
[*j,0*] is Element of COMPLEX
inv y is Element of REAL
* (j,(inv y)) is Element of REAL
* (y,(inv y)) is Element of REAL
* ((* (y,(inv y))),(inv y)) is Element of REAL
* ((inv y),(inv y)) is Element of REAL
* (y,(* ((inv y),(inv y)))) is Element of REAL
inv (* (y,y)) is Element of REAL
* (y,(inv (* (y,y)))) is Element of REAL
+ ((* (y,y)),0) is Element of REAL
inv (+ ((* (y,y)),0)) is Element of REAL
* (y,(inv (+ ((* (y,y)),0)))) is Element of REAL
inv (opp j) is Element of REAL
* ((* (y,y)),(inv (opp j))) is Element of REAL
+ ((* ((* (y,y)),(inv (opp j)))),(opp j)) is Element of REAL
j is Element of REAL
* ((opp j),j) is Element of REAL
+ ((* ((* (y,y)),(inv (opp j)))),(* ((opp j),j))) is Element of REAL
* ((opp j),(inv (opp j))) is Element of REAL
* ((opp j),(* ((opp j),(inv (opp j))))) is Element of REAL
+ ((* ((* (y,y)),(inv (opp j)))),(* ((opp j),(* ((opp j),(inv (opp j))))))) is Element of REAL
* ((opp j),(opp j)) is Element of REAL
* ((* ((opp j),(opp j))),(inv (opp j))) is Element of REAL
+ ((* ((* (y,y)),(inv (opp j)))),(* ((* ((opp j),(opp j))),(inv (opp j))))) is Element of REAL
+ ((* (y,y)),(* ((opp j),(opp j)))) is Element of REAL
* ((inv (opp j)),(+ ((* (y,y)),(* ((opp j),(opp j)))))) is Element of REAL
v1 is Element of REAL
[*v1,0*] is Element of COMPLEX
* (y,u2) is Element of REAL
* (j,u1) is Element of REAL
opp (* (j,u1)) is Element of REAL
* ((opp j),u1) is Element of REAL
* ((* (y,u2)),(inv (opp j))) is Element of REAL
* (u2,(inv (opp j))) is Element of REAL
* (y,(* (u2,(inv (opp j))))) is Element of REAL
* (y,(* (y,(* (u2,(inv (opp j))))))) is Element of REAL
* (j,u2) is Element of REAL
opp (* (j,u2)) is Element of REAL
+ ((* (y,(* (y,(* (u2,(inv (opp j)))))))),(opp (* (j,u2)))) is Element of REAL
* ((* (y,y)),(* (u2,(inv (opp j))))) is Element of REAL
+ ((* ((* (y,y)),(* (u2,(inv (opp j)))))),(opp (* (j,u2)))) is Element of REAL
* ((opp j),u2) is Element of REAL
+ ((* ((* (y,y)),(* (u2,(inv (opp j)))))),(* ((opp j),u2))) is Element of REAL
* (u2,(* ((* (y,y)),(inv (opp j))))) is Element of REAL
+ ((* (u2,(* ((* (y,y)),(inv (opp j)))))),(* ((opp j),u2))) is Element of REAL
* (u2,(+ ((* ((* (y,y)),(inv (opp j)))),(opp j)))) is Element of REAL
inv (+ ((* ((* (y,y)),(inv (opp j)))),(opp j))) is Element of REAL
* ((+ ((* ((* (y,y)),(inv (opp j)))),(opp j))),(opp j)) is Element of REAL
inv (* ((+ ((* ((* (y,y)),(inv (opp j)))),(opp j))),(opp j))) is Element of REAL
* (y,(inv (* ((+ ((* ((* (y,y)),(inv (opp j)))),(opp j))),(opp j))))) is Element of REAL
* ((* ((* (y,y)),(inv (opp j)))),(opp j)) is Element of REAL
+ ((* ((* ((* (y,y)),(inv (opp j)))),(opp j))),(* ((opp j),(opp j)))) is Element of REAL
inv (+ ((* ((* ((* (y,y)),(inv (opp j)))),(opp j))),(* ((opp j),(opp j))))) is Element of REAL
* (y,(inv (+ ((* ((* ((* (y,y)),(inv (opp j)))),(opp j))),(* ((opp j),(opp j))))))) is Element of REAL
* (j,(opp j)) is Element of REAL
opp (* (j,(opp j))) is Element of REAL
+ ((* ((* ((* (y,y)),(inv (opp j)))),(opp j))),(opp (* (j,(opp j))))) is Element of REAL
inv (+ ((* ((* ((* (y,y)),(inv (opp j)))),(opp j))),(opp (* (j,(opp j)))))) is Element of REAL
* (y,(inv (+ ((* ((* ((* (y,y)),(inv (opp j)))),(opp j))),(opp (* (j,(opp j)))))))) is Element of REAL
opp (* (j,j)) is Element of REAL
opp (opp (* (j,j))) is Element of REAL
+ ((* ((* ((* (y,y)),(inv (opp j)))),(opp j))),(opp (opp (* (j,j))))) is Element of REAL
inv (+ ((* ((* ((* (y,y)),(inv (opp j)))),(opp j))),(opp (opp (* (j,j)))))) is Element of REAL
* (y,(inv (+ ((* ((* ((* (y,y)),(inv (opp j)))),(opp j))),(opp (opp (* (j,j)))))))) is Element of REAL
* ((inv (opp j)),(opp j)) is Element of REAL
* ((* (y,y)),(* ((inv (opp j)),(opp j)))) is Element of REAL
+ ((* ((* (y,y)),(* ((inv (opp j)),(opp j))))),(* (j,j))) is Element of REAL
inv (+ ((* ((* (y,y)),(* ((inv (opp j)),(opp j))))),(* (j,j)))) is Element of REAL
* (y,(inv (+ ((* ((* (y,y)),(* ((inv (opp j)),(opp j))))),(* (j,j)))))) is Element of REAL
* ((* (y,y)),v1) is Element of REAL
+ ((* ((* (y,y)),v1)),(* (j,j))) is Element of REAL
inv (+ ((* ((* (y,y)),v1)),(* (j,j)))) is Element of REAL
* (y,(inv (+ ((* ((* (y,y)),v1)),(* (j,j)))))) is Element of REAL
* (v1,(inv (+ ((* ((* (y,y)),(inv (opp j)))),(opp j))))) is Element of REAL
* ((* ((opp j),(inv (opp j)))),(inv (+ ((* ((* (y,y)),(inv (opp j)))),(opp j))))) is Element of REAL
* ((inv (opp j)),(inv (+ ((* ((* (y,y)),(inv (opp j)))),(opp j))))) is Element of REAL
* ((opp j),(* ((inv (opp j)),(inv (+ ((* ((* (y,y)),(inv (opp j)))),(opp j))))))) is Element of REAL
* ((opp j),(+ ((* ((* (y,y)),(inv (opp j)))),(opp j)))) is Element of REAL
inv (* ((opp j),(+ ((* ((* (y,y)),(inv (opp j)))),(opp j))))) is Element of REAL
* ((opp j),(inv (* ((opp j),(+ ((* ((* (y,y)),(inv (opp j)))),(opp j))))))) is Element of REAL
* ((opp j),(* ((* (y,y)),(inv (opp j))))) is Element of REAL
+ ((* ((opp j),(* ((* (y,y)),(inv (opp j)))))),(* ((opp j),(opp j)))) is Element of REAL
inv (+ ((* ((opp j),(* ((* (y,y)),(inv (opp j)))))),(* ((opp j),(opp j))))) is Element of REAL
* ((opp j),(inv (+ ((* ((opp j),(* ((* (y,y)),(inv (opp j)))))),(* ((opp j),(opp j))))))) is Element of REAL
* ((* (y,y)),(* ((opp j),(inv (opp j))))) is Element of REAL
+ ((* ((* (y,y)),(* ((opp j),(inv (opp j)))))),(* ((opp j),(opp j)))) is Element of REAL
inv (+ ((* ((* (y,y)),(* ((opp j),(inv (opp j)))))),(* ((opp j),(opp j))))) is Element of REAL
* ((opp j),(inv (+ ((* ((* (y,y)),(* ((opp j),(inv (opp j)))))),(* ((opp j),(opp j))))))) is Element of REAL
+ ((* ((* (y,y)),v1)),(* ((opp j),(opp j)))) is Element of REAL
inv (+ ((* ((* (y,y)),v1)),(* ((opp j),(opp j))))) is Element of REAL
* ((opp j),(inv (+ ((* ((* (y,y)),v1)),(* ((opp j),(opp j))))))) is Element of REAL
inv (+ ((* (y,y)),(* ((opp j),(opp j))))) is Element of REAL
* ((opp j),(inv (+ ((* (y,y)),(* ((opp j),(opp j))))))) is Element of REAL
+ ((* (y,y)),(opp (* (j,(opp j))))) is Element of REAL
inv (+ ((* (y,y)),(opp (* (j,(opp j)))))) is Element of REAL
* ((opp j),(inv (+ ((* (y,y)),(opp (* (j,(opp j)))))))) is Element of REAL
+ ((* (y,y)),(opp (opp (* (j,j))))) is Element of REAL
inv (+ ((* (y,y)),(opp (opp (* (j,j)))))) is Element of REAL
* ((opp j),(inv (+ ((* (y,y)),(opp (opp (* (j,j)))))))) is Element of REAL
u2 is () set
u1 is () set
(u2,u1) is () set
(u1,u2) is () set
v1 is Element of REAL
v2 is Element of REAL
[*v1,v2*] is Element of COMPLEX
z is Element of REAL
u1 is Element of REAL
[*z,u1*] is Element of COMPLEX
* (v1,z) is Element of REAL
* (v2,u1) is Element of REAL
opp (* (v2,u1)) is Element of REAL
+ ((* (v1,z)),(opp (* (v2,u1)))) is Element of REAL
* (v1,u1) is Element of REAL
* (v2,z) is Element of REAL
+ ((* (v1,u1)),(* (v2,z))) is Element of REAL
[*(+ ((* (v1,z)),(opp (* (v2,u1))))),(+ ((* (v1,u1)),(* (v2,z))))*] is Element of COMPLEX
n is () set
y is () set
(y) is () set
(n,(y)) is () set
(y) is () set
(n,(y)) is () set
n is () set
y is () set
(n,y) is set
(y) is () set
(n,(y)) is () set
(n,y) is set
(y) is () set
(n,(y)) is () set
n is () set
y is () set
j is () set
(y,j) is () set
(n,(y,j)) is () set
(n,y) is () set
((n,y),j) is () set
u1 is Element of REAL
u2 is Element of REAL
[*u1,u2*] is Element of COMPLEX
v1 is Element of REAL
v2 is Element of REAL
[*v1,v2*] is Element of COMPLEX
* (u1,v1) is Element of REAL
* (u2,v2) is Element of REAL
opp (* (u2,v2)) is Element of REAL
+ ((* (u1,v1)),(opp (* (u2,v2)))) is Element of REAL
* (u1,v2) is Element of REAL
* (u2,v1) is Element of REAL
+ ((* (u1,v2)),(* (u2,v1))) is Element of REAL
[*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] is Element of COMPLEX
z is Element of REAL
u1 is Element of REAL
[*z,u1*] is Element of COMPLEX
u2 is Element of REAL
v1 is Element of REAL
[*u2,v1*] is Element of COMPLEX
* (z,u2) is Element of REAL
* (u1,v1) is Element of REAL
opp (* (u1,v1)) is Element of REAL
+ ((* (z,u2)),(opp (* (u1,v1)))) is Element of REAL
* (z,v1) is Element of REAL
* (u1,u2) is Element of REAL
+ ((* (z,v1)),(* (u1,u2))) is Element of REAL
[*(+ ((* (z,u2)),(opp (* (u1,v1))))),(+ ((* (z,v1)),(* (u1,u2))))*] is Element of COMPLEX
v2 is Element of REAL
x4 is Element of REAL
[*v2,x4*] is Element of COMPLEX
yz1 is Element of REAL
yz2 is Element of REAL
[*yz1,yz2*] is Element of COMPLEX
* (v2,yz1) is Element of REAL
* (x4,yz2) is Element of REAL
opp (* (x4,yz2)) is Element of REAL
+ ((* (v2,yz1)),(opp (* (x4,yz2)))) is Element of REAL
* (v2,yz2) is Element of REAL
* (x4,yz1) is Element of REAL
+ ((* (v2,yz2)),(* (x4,yz1))) is Element of REAL
[*(+ ((* (v2,yz1)),(opp (* (x4,yz2))))),(+ ((* (v2,yz2)),(* (x4,yz1))))*] is Element of COMPLEX
xy1 is Element of REAL
xy2 is Element of REAL
[*xy1,xy2*] is Element of COMPLEX
z3 is Element of REAL
z4 is Element of REAL
[*z3,z4*] is Element of COMPLEX
* (xy1,z3) is Element of REAL
* (xy2,z4) is Element of REAL
opp (* (xy2,z4)) is Element of REAL
+ ((* (xy1,z3)),(opp (* (xy2,z4)))) is Element of REAL
* (xy1,z4) is Element of REAL
* (xy2,z3) is Element of REAL
+ ((* (xy1,z4)),(* (xy2,z3))) is Element of REAL
[*(+ ((* (xy1,z3)),(opp (* (xy2,z4))))),(+ ((* (xy1,z4)),(* (xy2,z3))))*] is Element of COMPLEX
opp x4 is Element of REAL
* ((opp x4),(* (z,v1))) is Element of REAL
* ((opp x4),(* (u1,u2))) is Element of REAL
+ ((* ((opp x4),(* (z,v1)))),(* ((opp x4),(* (u1,u2))))) is Element of REAL
opp u2 is Element of REAL
* ((opp u2),v1) is Element of REAL
* ((* ((opp u2),v1)),z4) is Element of REAL
+ ((* ((opp x4),(* (u1,u2)))),(* ((* ((opp u2),v1)),z4))) is Element of REAL
* ((opp u2),v2) is Element of REAL
* ((* ((opp u2),v2)),z3) is Element of REAL
+ ((* ((* ((opp u2),v2)),z3)),(* ((* ((opp u2),v1)),z4))) is Element of REAL
opp u1 is Element of REAL
* ((opp u1),v1) is Element of REAL
* (v2,(* ((opp u1),v1))) is Element of REAL
+ ((* (v2,(* ((opp u1),v1)))),(+ ((* ((opp x4),(* (z,v1)))),(* ((opp x4),(* (u1,u2))))))) is Element of REAL
opp v2 is Element of REAL
* (u1,(opp v2)) is Element of REAL
* ((* (u1,(opp v2))),z4) is Element of REAL
+ ((* ((* (u1,(opp v2))),z4)),(+ ((* ((* ((opp u2),v2)),z3)),(* ((* ((opp u2),v1)),z4))))) is Element of REAL
opp (* (u1,v2)) is Element of REAL
* ((opp (* (u1,v2))),z4) is Element of REAL
+ ((* ((opp (* (u1,v2))),z4)),(+ ((* ((* ((opp u2),v2)),z3)),(* ((* ((opp u2),v1)),z4))))) is Element of REAL
opp u1 is Element of REAL
* ((opp u1),v2) is Element of REAL
* ((* ((opp u1),v2)),z4) is Element of REAL
+ ((* ((* ((opp u1),v2)),z4)),(+ ((* ((* ((opp u2),v2)),z3)),(* ((* ((opp u2),v1)),z4))))) is Element of REAL
+ ((* ((* ((opp u1),v2)),z4)),(* ((* ((opp u2),v1)),z4))) is Element of REAL
+ ((* ((* ((opp u2),v2)),z3)),(+ ((* ((* ((opp u1),v2)),z4)),(* ((* ((opp u2),v1)),z4))))) is Element of REAL
* ((opp x4),yz2) is Element of REAL
+ ((* (v2,yz1)),(* ((opp x4),yz2))) is Element of REAL
+ ((* (z,u2)),(* ((opp u1),v1))) is Element of REAL
* (v2,(+ ((* (z,u2)),(* ((opp u1),v1))))) is Element of REAL
+ ((* (v2,(+ ((* (z,u2)),(* ((opp u1),v1)))))),(* ((opp x4),yz2))) is Element of REAL
* (v2,(* (z,u2))) is Element of REAL
+ ((* (v2,(* (z,u2)))),(* (v2,(* ((opp u1),v1))))) is Element of REAL
* ((opp x4),(+ ((* (z,v1)),(* (u1,u2))))) is Element of REAL
+ ((+ ((* (v2,(* (z,u2)))),(* (v2,(* ((opp u1),v1)))))),(* ((opp x4),(+ ((* (z,v1)),(* (u1,u2))))))) is Element of REAL
+ ((+ ((* (v2,(* (z,u2)))),(* (v2,(* ((opp u1),v1)))))),(+ ((* ((opp x4),(* (z,v1)))),(* ((opp x4),(* (u1,u2))))))) is Element of REAL
+ ((* (v2,(* (z,u2)))),(+ ((* ((* ((opp u2),v2)),z3)),(+ ((* ((* ((opp u1),v2)),z4)),(* ((* ((opp u2),v1)),z4))))))) is Element of REAL
+ ((* (v2,(* (z,u2)))),(* ((* ((opp u2),v2)),z3))) is Element of REAL
+ ((+ ((* (v2,(* (z,u2)))),(* ((* ((opp u2),v2)),z3)))),(+ ((* ((* ((opp u1),v2)),z4)),(* ((* ((opp u2),v1)),z4))))) is Element of REAL
* ((* (u1,v1)),z3) is Element of REAL
+ ((* ((* (u1,v1)),z3)),(* ((* ((opp u2),v2)),z3))) is Element of REAL
+ ((+ ((* ((* (u1,v1)),z3)),(* ((* ((opp u2),v2)),z3)))),(+ ((* ((* ((opp u1),v2)),z4)),(* ((* ((opp u2),v1)),z4))))) is Element of REAL
+ ((* (u1,v1)),(* ((opp u2),v2))) is Element of REAL
* ((+ ((* (u1,v1)),(* ((opp u2),v2)))),z3) is Element of REAL
+ ((* ((+ ((* (u1,v1)),(* ((opp u2),v2)))),z3)),(+ ((* ((* ((opp u1),v2)),z4)),(* ((* ((opp u2),v1)),z4))))) is Element of REAL
opp (* (u2,v1)) is Element of REAL
* ((opp (* (u2,v1))),z4) is Element of REAL
+ ((* ((* ((opp u1),v2)),z4)),(* ((opp (* (u2,v1))),z4))) is Element of REAL
+ ((* ((+ ((* (u1,v1)),(* ((opp u2),v2)))),z3)),(+ ((* ((* ((opp u1),v2)),z4)),(* ((opp (* (u2,v1))),z4))))) is Element of REAL
* ((* (u2,v1)),z4) is Element of REAL
opp (* ((* (u2,v1)),z4)) is Element of REAL
+ ((* ((* ((opp u1),v2)),z4)),(opp (* ((* (u2,v1)),z4)))) is Element of REAL
+ ((* ((+ ((* (u1,v1)),(* ((opp u2),v2)))),z3)),(+ ((* ((* ((opp u1),v2)),z4)),(opp (* ((* (u2,v1)),z4)))))) is Element of REAL
+ ((* ((opp (* (u1,v2))),z4)),(opp (* ((* (u2,v1)),z4)))) is Element of REAL
+ ((* ((+ ((* (u1,v1)),(* ((opp u2),v2)))),z3)),(+ ((* ((opp (* (u1,v2))),z4)),(opp (* ((* (u2,v1)),z4)))))) is Element of REAL
* ((* (u1,v2)),z4) is Element of REAL
opp (* ((* (u1,v2)),z4)) is Element of REAL
+ ((opp (* ((* (u1,v2)),z4))),(opp (* ((* (u2,v1)),z4)))) is Element of REAL
+ ((* ((+ ((* (u1,v1)),(* ((opp u2),v2)))),z3)),(+ ((opp (* ((* (u1,v2)),z4))),(opp (* ((* (u2,v1)),z4)))))) is Element of REAL
+ ((* ((* (u1,v2)),z4)),(* ((* (u2,v1)),z4))) is Element of REAL
opp (+ ((* ((* (u1,v2)),z4)),(* ((* (u2,v1)),z4)))) is Element of REAL
+ ((* ((+ ((* (u1,v1)),(* ((opp u2),v2)))),z3)),(opp (+ ((* ((* (u1,v2)),z4)),(* ((* (u2,v1)),z4)))))) is Element of REAL
* ((+ ((* (u1,v2)),(* (u2,v1)))),z4) is Element of REAL
opp (* ((+ ((* (u1,v2)),(* (u2,v1)))),z4)) is Element of REAL
+ ((* ((+ ((* (u1,v1)),(* ((opp u2),v2)))),z3)),(opp (* ((+ ((* (u1,v2)),(* (u2,v1)))),z4)))) is Element of REAL
opp xy2 is Element of REAL
* ((opp xy2),z4) is Element of REAL
+ ((* ((+ ((* (u1,v1)),(* ((opp u2),v2)))),z3)),(* ((opp xy2),z4))) is Element of REAL
+ ((* (xy1,z3)),(* ((opp xy2),z4))) is Element of REAL
* ((opp (* (u2,v2))),z4) is Element of REAL
* ((* (u2,v1)),z3) is Element of REAL
+ ((* ((opp (* (u2,v2))),z4)),(* ((* (u2,v1)),z3))) is Element of REAL
* ((* (u2,v2)),z4) is Element of REAL
opp (* ((* (u2,v2)),z4)) is Element of REAL
+ ((opp (* ((* (u2,v2)),z4))),(* ((* (u2,v1)),z3))) is Element of REAL
* (x4,(* (z,u2))) is Element of REAL
+ ((* (x4,(* (z,u2)))),(opp (* ((* (u2,v2)),z4)))) is Element of REAL
* (x4,(* (u1,v1))) is Element of REAL
opp (* (x4,(* (u1,v1)))) is Element of REAL
+ ((* (x4,(* (z,u2)))),(opp (* (x4,(* (u1,v1)))))) is Element of REAL
* (x4,(opp (* (u1,v1)))) is Element of REAL
+ ((* (x4,(* (z,u2)))),(* (x4,(opp (* (u1,v1)))))) is Element of REAL
+ ((* ((opp (* (u2,v2))),z4)),(* (xy2,z3))) is Element of REAL
* ((* (u1,v2)),z3) is Element of REAL
+ ((* ((* (u1,v2)),z3)),(* ((* (u2,v1)),z3))) is Element of REAL
+ ((* ((opp (* (u2,v2))),z4)),(+ ((* ((* (u1,v2)),z3)),(* ((* (u2,v1)),z3))))) is Element of REAL
+ ((* ((* (u1,v2)),z3)),(+ ((* ((opp (* (u2,v2))),z4)),(* ((* (u2,v1)),z3))))) is Element of REAL
* (v2,(* (u1,u2))) is Element of REAL
+ ((* (v2,(* (u1,u2)))),(+ ((* (x4,(* (z,u2)))),(* (x4,(opp (* (u1,v1)))))))) is Element of REAL
+ ((* (v2,(* (u1,u2)))),(* (x4,yz1))) is Element of REAL
* ((* (u1,v1)),z4) is Element of REAL
+ ((* ((* (u1,v1)),z4)),(* ((opp (* (u2,v2))),z4))) is Element of REAL
+ ((+ ((* ((* (u1,v1)),z4)),(* ((opp (* (u2,v2))),z4)))),(* (xy2,z3))) is Element of REAL
+ ((* ((* (u1,v1)),z4)),(+ ((* ((opp (* (u2,v2))),z4)),(* (xy2,z3))))) is Element of REAL
* (v2,(* (z,v1))) is Element of REAL
+ ((* (v2,(* (z,v1)))),(+ ((* (v2,(* (u1,u2)))),(* (x4,yz1))))) is Element of REAL
+ ((* (v2,(* (z,v1)))),(* (v2,(* (u1,u2))))) is Element of REAL
+ ((+ ((* (v2,(* (z,v1)))),(* (v2,(* (u1,u2)))))),(* (x4,yz1))) is Element of REAL
n is non empty () set
(n) is () set
(n,(n)) is () set
y is Element of REAL
j is Element of REAL
[*y,j*] is Element of COMPLEX
u1 is Element of REAL
u2 is Element of REAL
[*u1,u2*] is Element of COMPLEX
+ (y,u1) is Element of REAL
+ (j,u2) is Element of REAL
[*(+ (y,u1)),(+ (j,u2))*] is Element of COMPLEX
(n) is () set
(n,(n)) is () set
y is Element of REAL
j is Element of REAL
[*y,j*] is Element of COMPLEX
u1 is Element of REAL
u2 is Element of REAL
[*u1,u2*] is Element of COMPLEX
* (y,u1) is Element of REAL
* (j,u2) is Element of REAL
opp (* (j,u2)) is Element of REAL
+ ((* (y,u1)),(opp (* (j,u2)))) is Element of REAL
* (y,u2) is Element of REAL
* (j,u1) is Element of REAL
+ ((* (y,u2)),(* (j,u1))) is Element of REAL
[*(+ ((* (y,u1)),(opp (* (j,u2))))),(+ ((* (y,u2)),(* (j,u1))))*] is Element of COMPLEX
opp j is Element of REAL
* ((opp j),u2) is Element of REAL
+ ((* (y,u1)),(* ((opp j),u2))) is Element of REAL
y is non empty () set
(n,y) is () set
j is () set
(j,y) is () set
u1 is Element of REAL
u2 is Element of REAL
[*u1,u2*] is Element of COMPLEX
v1 is Element of REAL
v2 is Element of REAL
[*v1,v2*] is Element of COMPLEX
* (u1,v1) is Element of REAL
* (u2,v2) is Element of REAL
opp (* (u2,v2)) is Element of REAL
+ ((* (u1,v1)),(opp (* (u2,v2)))) is Element of REAL
* (u1,v2) is Element of REAL
* (u2,v1) is Element of REAL
+ ((* (u1,v2)),(* (u2,v1))) is Element of REAL
[*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] is Element of COMPLEX
opp 0 is Element of REAL
+ (0,(opp 0)) is Element of REAL
+ (v1,(opp (* (u2,v2)))) is Element of REAL
opp u2 is Element of REAL
* ((opp u2),v2) is Element of REAL
+ (v1,(* ((opp u2),v2))) is Element of REAL
* (0,v2) is Element of REAL
+ (v1,(* (0,v2))) is Element of REAL
z is () set
((n),z) is () set
u1 is Element of REAL
u2 is Element of REAL
[*u1,u2*] is Element of COMPLEX
v1 is Element of REAL
v2 is Element of REAL
[*v1,v2*] is Element of COMPLEX
* (u1,v1) is Element of REAL
* (u2,v2) is Element of REAL
opp (* (u2,v2)) is Element of REAL
+ ((* (u1,v1)),(opp (* (u2,v2)))) is Element of REAL
* (u1,v2) is Element of REAL
* (u2,v1) is Element of REAL
+ ((* (u1,v2)),(* (u2,v1))) is Element of REAL
[*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] is Element of COMPLEX
+ (0,(* (u2,v1))) is Element of REAL
((n),n) is () set
(((n),n),y) is () set
((n),(n,y)) is () set
n is non empty () set
y is non empty () set
(n,y) is () set
(y) is non empty () set
(n,(y)) is non empty () set
n is Element of REAL
n is set
n is Element of COMPLEX