:: COMPLFLD semantic presentation

REAL is non empty V39() set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V39() set
RAT is non empty V39() set
INT is non empty V39() set
K20(COMPLEX,COMPLEX) is set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(REAL,REAL) is set
K19(K20(REAL,REAL)) is set
K20(K20(REAL,REAL),REAL) is set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is set
K20(K20(NAT,NAT),NAT) is set
K19(K20(K20(NAT,NAT),NAT)) is set
omega is non empty epsilon-transitive epsilon-connected ordinal set
K19(omega) is set
K19(NAT) is set
{} is empty ext-real non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V35() set
1 is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
0 is empty ext-real non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V35() Element of NAT
0 *' is complex Element of COMPLEX
Re 0 is ext-real complex V35() Element of REAL
Im 0 is ext-real complex V35() Element of REAL
<i> is complex Element of COMPLEX
(Im 0) * <i> is complex set
(Re 0) - ((Im 0) * <i>) is complex set
1r is complex Element of COMPLEX
1r *' is complex Element of COMPLEX
Re 1r is ext-real complex V35() Element of REAL
Im 1r is ext-real complex V35() Element of REAL
(Im 1r) * <i> is complex set
(Re 1r) - ((Im 1r) * <i>) is complex set
|.0.| is empty ext-real non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V35() Element of REAL
|.1r.| is ext-real non negative complex V35() Element of REAL
addcomplex is V1() V4(K20(COMPLEX,COMPLEX)) V5( COMPLEX ) Function-like V18(K20(COMPLEX,COMPLEX), COMPLEX ) Element of K19(K20(K20(COMPLEX,COMPLEX),COMPLEX))
multcomplex is V1() V4(K20(COMPLEX,COMPLEX)) V5( COMPLEX ) Function-like V18(K20(COMPLEX,COMPLEX), COMPLEX ) Element of K19(K20(K20(COMPLEX,COMPLEX),COMPLEX))
0c is empty ext-real non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V35() Element of COMPLEX
doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) is strict doubleLoopStr
the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) is set
the addF of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) is V1() V4(K20( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #))) V5( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)) Function-like V18(K20( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)) Element of K19(K20(K20( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)))
K20( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)) is set
K20(K20( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)) is set
K19(K20(K20( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #))) is set
the multF of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) is V1() V4(K20( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #))) V5( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)) Function-like V18(K20( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)) Element of K19(K20(K20( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)), the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)))
1. doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) is Element of the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)
the OneF of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) is Element of the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)
0. doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) is zero Element of the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)
the ZeroF of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) is Element of the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)
n is strict doubleLoopStr
the carrier of n is set
the addF of n is V1() V4(K20( the carrier of n, the carrier of n)) V5( the carrier of n) Function-like V18(K20( the carrier of n, the carrier of n), the carrier of n) Element of K19(K20(K20( the carrier of n, the carrier of n), the carrier of n))
K20( the carrier of n, the carrier of n) is set
K20(K20( the carrier of n, the carrier of n), the carrier of n) is set
K19(K20(K20( the carrier of n, the carrier of n), the carrier of n)) is set
the multF of n is V1() V4(K20( the carrier of n, the carrier of n)) V5( the carrier of n) Function-like V18(K20( the carrier of n, the carrier of n), the carrier of n) Element of K19(K20(K20( the carrier of n, the carrier of n), the carrier of n))
1. n is Element of the carrier of n
the OneF of n is Element of the carrier of n
0. n is zero Element of the carrier of n
the ZeroF of n is Element of the carrier of n
x is strict doubleLoopStr
the carrier of x is set
the addF of x is V1() V4(K20( the carrier of x, the carrier of x)) V5( the carrier of x) Function-like V18(K20( the carrier of x, the carrier of x), the carrier of x) Element of K19(K20(K20( the carrier of x, the carrier of x), the carrier of x))
K20( the carrier of x, the carrier of x) is set
K20(K20( the carrier of x, the carrier of x), the carrier of x) is set
K19(K20(K20( the carrier of x, the carrier of x), the carrier of x)) is set
the multF of x is V1() V4(K20( the carrier of x, the carrier of x)) V5( the carrier of x) Function-like V18(K20( the carrier of x, the carrier of x), the carrier of x) Element of K19(K20(K20( the carrier of x, the carrier of x), the carrier of x))
1. x is Element of the carrier of x
the OneF of x is Element of the carrier of x
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
() is strict doubleLoopStr
the carrier of () is non empty set
n is Element of the carrier of ()
v is complex Element of the carrier of ()
n is complex set
t is complex Element of the carrier of ()
x is complex set
v + t is complex Element of the carrier of ()
the addF of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) Function-like V18(K20( the carrier of (), the carrier of ()), the carrier of ()) Element of K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ()))
K20( the carrier of (), the carrier of ()) is set
K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set
K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set
the addF of () . (v,t) is complex Element of the carrier of ()
[v,t] is set
the addF of () . [v,t] is set
n + x is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
addcomplex . (t,t) is complex Element of COMPLEX
[t,t] is set
addcomplex . [t,t] is set
v + t is complex Element of COMPLEX
v * t is complex Element of the carrier of ()
the multF of () is V1() V4(K20( the carrier of (), the carrier of ())) V5( the carrier of ()) Function-like V18(K20( the carrier of (), the carrier of ()), the carrier of ()) Element of K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ()))
the multF of () . (v,t) is complex Element of the carrier of ()
the multF of () . [v,t] is set
n * x is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
multcomplex . (t,t) is complex Element of COMPLEX
[t,t] is set
multcomplex . [t,t] is set
v * t is complex Element of COMPLEX
n is complex Element of the carrier of ()
1. () is complex Element of the carrier of ()
the OneF of () is complex Element of the carrier of ()
n * (1. ()) is complex Element of the carrier of ()
the multF of () . (n,(1. ())) is complex Element of the carrier of ()
[n,(1. ())] is set
the multF of () . [n,(1. ())] is set
n * (1. ()) is complex Element of COMPLEX
(1. ()) * n is complex Element of the carrier of ()
the multF of () . ((1. ()),n) is complex Element of the carrier of ()
[(1. ()),n] is set
the multF of () . [(1. ()),n] is set
(1. ()) * n is complex Element of COMPLEX
1_ () is complex Element of the carrier of ()
1. () is complex Element of the carrier of ()
the OneF of () is complex Element of the carrier of ()
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n + x is complex Element of the carrier of ()
the addF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the addF of () . [n,x] is set
n + x is complex Element of COMPLEX
v is complex Element of the carrier of ()
(n + x) + v is complex Element of the carrier of ()
the addF of () . ((n + x),v) is complex Element of the carrier of ()
[(n + x),v] is set
the addF of () . [(n + x),v] is set
(n + x) + v is complex Element of COMPLEX
x + v is complex Element of the carrier of ()
the addF of () . (x,v) is complex Element of the carrier of ()
[x,v] is set
the addF of () . [x,v] is set
x + v is complex Element of COMPLEX
n + (x + v) is complex Element of the carrier of ()
the addF of () . (n,(x + v)) is complex Element of the carrier of ()
[n,(x + v)] is set
the addF of () . [n,(x + v)] is set
n + (x + v) is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
[t,t] is set
the addF of () . [t,t] is set
t is complex Element of COMPLEX
[( the addF of () . [t,t]),t] is set
addcomplex . [( the addF of () . [t,t]),t] is set
addcomplex . (t,t) is complex Element of COMPLEX
addcomplex . [t,t] is set
addcomplex . ((addcomplex . (t,t)),t) is complex Element of COMPLEX
[(addcomplex . (t,t)),t] is set
addcomplex . [(addcomplex . (t,t)),t] is set
t + t is complex Element of COMPLEX
addcomplex . ((t + t),t) is complex Element of COMPLEX
[(t + t),t] is set
addcomplex . [(t + t),t] is set
(t + t) + t is complex Element of COMPLEX
t + t is complex Element of COMPLEX
t + (t + t) is complex Element of COMPLEX
addcomplex . (t,(t + t)) is complex Element of COMPLEX
[t,(t + t)] is set
addcomplex . [t,(t + t)] is set
addcomplex . (t,t) is complex Element of COMPLEX
[t,t] is set
addcomplex . [t,t] is set
[t,(addcomplex . (t,t))] is set
addcomplex . [t,(addcomplex . (t,t))] is set
the addF of () . [t,t] is set
[t,( the addF of () . [t,t])] is set
addcomplex . [t,( the addF of () . [t,t])] is set
n is complex Element of the carrier of ()
0. () is complex zero Element of the carrier of ()
the ZeroF of () is complex Element of the carrier of ()
n + (0. ()) is complex Element of the carrier of ()
the addF of () . (n,(0. ())) is complex Element of the carrier of ()
[n,(0. ())] is set
the addF of () . [n,(0. ())] is set
n + (0. ()) is complex Element of COMPLEX
x is complex Element of COMPLEX
the addF of () . (x,0c) is set
[x,0c] is set
the addF of () . [x,0c] is set
addcomplex . (x,0c) is complex Element of COMPLEX
addcomplex . [x,0c] is set
x + 0c is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of COMPLEX
- x is complex Element of COMPLEX
v is complex Element of the carrier of ()
n + v is complex Element of the carrier of ()
the addF of () . (n,v) is complex Element of the carrier of ()
[n,v] is set
the addF of () . [n,v] is set
n + v is complex Element of COMPLEX
0. () is complex zero Element of the carrier of ()
the ZeroF of () is complex Element of the carrier of ()
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n + x is complex Element of the carrier of ()
the addF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the addF of () . [n,x] is set
n + x is complex Element of COMPLEX
x + n is complex Element of the carrier of ()
the addF of () . (x,n) is complex Element of the carrier of ()
[x,n] is set
the addF of () . [x,n] is set
x + n is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
x * n is complex Element of the carrier of ()
the multF of () . (x,n) is complex Element of the carrier of ()
[x,n] is set
the multF of () . [x,n] is set
x * n is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
v is complex Element of the carrier of ()
(n * x) * v is complex Element of the carrier of ()
the multF of () . ((n * x),v) is complex Element of the carrier of ()
[(n * x),v] is set
the multF of () . [(n * x),v] is set
(n * x) * v is complex Element of COMPLEX
x * v is complex Element of the carrier of ()
the multF of () . (x,v) is complex Element of the carrier of ()
[x,v] is set
the multF of () . [x,v] is set
x * v is complex Element of COMPLEX
n * (x * v) is complex Element of the carrier of ()
the multF of () . (n,(x * v)) is complex Element of the carrier of ()
[n,(x * v)] is set
the multF of () . [n,(x * v)] is set
n * (x * v) is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
the multF of () . (t,t) is set
[t,t] is set
the multF of () . [t,t] is set
t is complex Element of COMPLEX
multcomplex . (( the multF of () . (t,t)),t) is set
[( the multF of () . (t,t)),t] is set
multcomplex . [( the multF of () . (t,t)),t] is set
multcomplex . (t,t) is complex Element of COMPLEX
multcomplex . [t,t] is set
multcomplex . ((multcomplex . (t,t)),t) is complex Element of COMPLEX
[(multcomplex . (t,t)),t] is set
multcomplex . [(multcomplex . (t,t)),t] is set
t * t is complex Element of COMPLEX
multcomplex . ((t * t),t) is complex Element of COMPLEX
[(t * t),t] is set
multcomplex . [(t * t),t] is set
(t * t) * t is complex Element of COMPLEX
t * t is complex Element of COMPLEX
t * (t * t) is complex Element of COMPLEX
multcomplex . (t,(t * t)) is complex Element of COMPLEX
[t,(t * t)] is set
multcomplex . [t,(t * t)] is set
multcomplex . (t,t) is complex Element of COMPLEX
[t,t] is set
multcomplex . [t,t] is set
multcomplex . (t,(multcomplex . (t,t))) is complex Element of COMPLEX
[t,(multcomplex . (t,t))] is set
multcomplex . [t,(multcomplex . (t,t))] is set
the multF of () . (t,t) is set
the multF of () . [t,t] is set
multcomplex . (t,( the multF of () . (t,t))) is set
[t,( the multF of () . (t,t))] is set
multcomplex . [t,( the multF of () . (t,t))] is set
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
v is complex Element of the carrier of ()
x + v is complex Element of the carrier of ()
the addF of () . (x,v) is complex Element of the carrier of ()
[x,v] is set
the addF of () . [x,v] is set
x + v is complex Element of COMPLEX
n * (x + v) is complex Element of the carrier of ()
the multF of () . (n,(x + v)) is complex Element of the carrier of ()
[n,(x + v)] is set
the multF of () . [n,(x + v)] is set
n * (x + v) is complex Element of COMPLEX
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
n * v is complex Element of the carrier of ()
the multF of () . (n,v) is complex Element of the carrier of ()
[n,v] is set
the multF of () . [n,v] is set
n * v is complex Element of COMPLEX
(n * x) + (n * v) is complex Element of the carrier of ()
the addF of () . ((n * x),(n * v)) is complex Element of the carrier of ()
[(n * x),(n * v)] is set
the addF of () . [(n * x),(n * v)] is set
(n * x) + (n * v) is complex Element of COMPLEX
(x + v) * n is complex Element of the carrier of ()
the multF of () . ((x + v),n) is complex Element of the carrier of ()
[(x + v),n] is set
the multF of () . [(x + v),n] is set
(x + v) * n is complex Element of COMPLEX
x * n is complex Element of the carrier of ()
the multF of () . (x,n) is complex Element of the carrier of ()
[x,n] is set
the multF of () . [x,n] is set
x * n is complex Element of COMPLEX
v * n is complex Element of the carrier of ()
the multF of () . (v,n) is complex Element of the carrier of ()
[v,n] is set
the multF of () . [v,n] is set
v * n is complex Element of COMPLEX
(x * n) + (v * n) is complex Element of the carrier of ()
the addF of () . ((x * n),(v * n)) is complex Element of the carrier of ()
[(x * n),(v * n)] is set
the addF of () . [(x * n),(v * n)] is set
(x * n) + (v * n) is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
the addF of () . (t,t) is set
[t,t] is set
the addF of () . [t,t] is set
multcomplex . (t,( the addF of () . (t,t))) is set
[t,( the addF of () . (t,t))] is set
multcomplex . [t,( the addF of () . (t,t))] is set
addcomplex . (t,t) is complex Element of COMPLEX
addcomplex . [t,t] is set
multcomplex . (t,(addcomplex . (t,t))) is complex Element of COMPLEX
[t,(addcomplex . (t,t))] is set
multcomplex . [t,(addcomplex . (t,t))] is set
t + t is complex Element of COMPLEX
multcomplex . (t,(t + t)) is complex Element of COMPLEX
[t,(t + t)] is set
multcomplex . [t,(t + t)] is set
t * (t + t) is complex Element of COMPLEX
t * t is complex Element of COMPLEX
t * t is complex Element of COMPLEX
(t * t) + (t * t) is complex Element of COMPLEX
addcomplex . ((t * t),(t * t)) is complex Element of COMPLEX
[(t * t),(t * t)] is set
addcomplex . [(t * t),(t * t)] is set
multcomplex . (t,t) is complex Element of COMPLEX
[t,t] is set
multcomplex . [t,t] is set
addcomplex . ((multcomplex . (t,t)),(t * t)) is complex Element of COMPLEX
[(multcomplex . (t,t)),(t * t)] is set
addcomplex . [(multcomplex . (t,t)),(t * t)] is set
multcomplex . (t,t) is complex Element of COMPLEX
[t,t] is set
multcomplex . [t,t] is set
addcomplex . ((multcomplex . (t,t)),(multcomplex . (t,t))) is complex Element of COMPLEX
[(multcomplex . (t,t)),(multcomplex . (t,t))] is set
addcomplex . [(multcomplex . (t,t)),(multcomplex . (t,t))] is set
the addF of () . ((multcomplex . (t,t)),(multcomplex . (t,t))) is set
the addF of () . [(multcomplex . (t,t)),(multcomplex . (t,t))] is set
the multF of () . (t,t) is set
the multF of () . [t,t] is set
the addF of () . (( the multF of () . (t,t)),(multcomplex . (t,t))) is set
[( the multF of () . (t,t)),(multcomplex . (t,t))] is set
the addF of () . [( the multF of () . (t,t)),(multcomplex . (t,t))] is set
multcomplex . (( the addF of () . (t,t)),t) is set
[( the addF of () . (t,t)),t] is set
multcomplex . [( the addF of () . (t,t)),t] is set
multcomplex . ((addcomplex . (t,t)),t) is complex Element of COMPLEX
[(addcomplex . (t,t)),t] is set
multcomplex . [(addcomplex . (t,t)),t] is set
multcomplex . ((t + t),t) is complex Element of COMPLEX
[(t + t),t] is set
multcomplex . [(t + t),t] is set
(t + t) * t is complex Element of COMPLEX
t * t is complex Element of COMPLEX
t * t is complex Element of COMPLEX
(t * t) + (t * t) is complex Element of COMPLEX
addcomplex . ((t * t),(t * t)) is complex Element of COMPLEX
[(t * t),(t * t)] is set
addcomplex . [(t * t),(t * t)] is set
multcomplex . (t,t) is complex Element of COMPLEX
[t,t] is set
multcomplex . [t,t] is set
addcomplex . ((multcomplex . (t,t)),(t * t)) is complex Element of COMPLEX
[(multcomplex . (t,t)),(t * t)] is set
addcomplex . [(multcomplex . (t,t)),(t * t)] is set
multcomplex . (t,t) is complex Element of COMPLEX
[t,t] is set
multcomplex . [t,t] is set
addcomplex . ((multcomplex . (t,t)),(multcomplex . (t,t))) is complex Element of COMPLEX
[(multcomplex . (t,t)),(multcomplex . (t,t))] is set
addcomplex . [(multcomplex . (t,t)),(multcomplex . (t,t))] is set
the addF of () . ((multcomplex . (t,t)),(multcomplex . (t,t))) is set
the addF of () . [(multcomplex . (t,t)),(multcomplex . (t,t))] is set
the multF of () . (t,t) is set
the multF of () . [t,t] is set
the addF of () . (( the multF of () . (t,t)),(multcomplex . (t,t))) is set
[( the multF of () . (t,t)),(multcomplex . (t,t))] is set
the addF of () . [( the multF of () . (t,t)),(multcomplex . (t,t))] is set
n is complex Element of the carrier of ()
0. () is complex zero Element of the carrier of ()
the ZeroF of () is complex Element of the carrier of ()
x is complex Element of COMPLEX
x " is complex Element of COMPLEX
v is complex Element of the carrier of ()
v * n is complex Element of the carrier of ()
the multF of () . (v,n) is complex Element of the carrier of ()
[v,n] is set
the multF of () . [v,n] is set
v * n is complex Element of COMPLEX
0. () is complex zero Element of the carrier of ()
the ZeroF of () is complex Element of the carrier of ()
n is complex Element of the carrier of ()
v is complex set
x is complex Element of the carrier of ()
t is complex set
n + x is complex Element of the carrier of ()
the addF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the addF of () . [n,x] is set
n + x is complex Element of COMPLEX
v + t is complex Element of COMPLEX
n is complex Element of the carrier of ()
- n is complex Element of the carrier of ()
x is complex set
- x is complex Element of COMPLEX
v is complex Element of COMPLEX
- v is complex Element of COMPLEX
t is complex Element of the carrier of ()
n + t is complex Element of the carrier of ()
the addF of () . (n,t) is complex Element of the carrier of ()
[n,t] is set
the addF of () . [n,t] is set
n + t is complex Element of COMPLEX
0. () is complex zero Element of the carrier of ()
the ZeroF of () is complex Element of the carrier of ()
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n - x is complex Element of the carrier of ()
- x is complex Element of the carrier of ()
n + (- x) is complex Element of the carrier of ()
the addF of () . (n,(- x)) is complex Element of the carrier of ()
[n,(- x)] is set
the addF of () . [n,(- x)] is set
n + (- x) is complex Element of COMPLEX
v is complex set
t is complex set
v - t is complex Element of COMPLEX
- t is complex Element of COMPLEX
n is complex Element of the carrier of ()
v is complex set
x is complex Element of the carrier of ()
t is complex set
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
v * t is complex Element of COMPLEX
0. () is complex zero Element of the carrier of ()
the ZeroF of () is complex Element of the carrier of ()
n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x is complex set
x " is complex Element of COMPLEX
v is complex Element of COMPLEX
v " is complex Element of COMPLEX
t is complex Element of the carrier of ()
n * t is complex Element of the carrier of ()
the multF of () . (n,t) is complex Element of the carrier of ()
[n,t] is set
the multF of () . [n,t] is set
n * t is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n / x is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
n * (x ") is complex Element of the carrier of ()
the multF of () . (n,(x ")) is complex Element of the carrier of ()
[n,(x ")] is set
the multF of () . [n,(x ")] is set
n * (x ") is complex Element of COMPLEX
v is complex set
t is complex set
v / t is complex Element of COMPLEX
t " is complex Element of COMPLEX
(1_ ()) + (1_ ()) is complex Element of the carrier of ()
the addF of () . ((1_ ()),(1_ ())) is complex Element of the carrier of ()
[(1_ ()),(1_ ())] is set
the addF of () . [(1_ ()),(1_ ())] is set
(1_ ()) + (1_ ()) is complex Element of COMPLEX
n is complex Element of the carrier of ()
n *' is complex set
Re n is ext-real complex V35() Element of REAL
Im n is ext-real complex V35() Element of REAL
(Im n) * <i> is complex set
(Re n) - ((Im n) * <i>) is complex set
n *' is complex Element of COMPLEX
- (1_ ()) is complex Element of the carrier of ()
n is complex Element of the carrier of ()
- n is complex Element of the carrier of ()
(- (1_ ())) * n is complex Element of the carrier of ()
the multF of () . ((- (1_ ())),n) is complex Element of the carrier of ()
[(- (1_ ())),n] is set
the multF of () . [(- (1_ ())),n] is set
(- (1_ ())) * n is complex Element of COMPLEX
- 1r is complex Element of COMPLEX
x is complex Element of COMPLEX
- x is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
- x is complex Element of the carrier of ()
n - (- x) is complex Element of the carrier of ()
- (- x) is complex Element of the carrier of ()
n + (- (- x)) is complex Element of the carrier of ()
the addF of () . (n,(- (- x))) is complex Element of the carrier of ()
[n,(- (- x))] is set
the addF of () . [n,(- (- x))] is set
n + (- (- x)) is complex Element of COMPLEX
n + x is complex Element of the carrier of ()
the addF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the addF of () . [n,x] is set
n + x is complex Element of COMPLEX
t is complex Element of COMPLEX
- t is complex Element of COMPLEX
v is complex Element of COMPLEX
v - (- t) is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n + x is complex Element of the carrier of ()
the addF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the addF of () . [n,x] is set
n + x is complex Element of COMPLEX
(n + x) - x is complex Element of the carrier of ()
- x is complex Element of the carrier of ()
(n + x) + (- x) is complex Element of the carrier of ()
the addF of () . ((n + x),(- x)) is complex Element of the carrier of ()
[(n + x),(- x)] is set
the addF of () . [(n + x),(- x)] is set
(n + x) + (- x) is complex Element of COMPLEX
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v + t is complex Element of COMPLEX
(v + t) - t is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n - x is complex Element of the carrier of ()
- x is complex Element of the carrier of ()
n + (- x) is complex Element of the carrier of ()
the addF of () . (n,(- x)) is complex Element of the carrier of ()
[n,(- x)] is set
the addF of () . [n,(- x)] is set
n + (- x) is complex Element of COMPLEX
(n - x) + x is complex Element of the carrier of ()
the addF of () . ((n - x),x) is complex Element of the carrier of ()
[(n - x),x] is set
the addF of () . [(n - x),x] is set
(n - x) + x is complex Element of COMPLEX
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v - t is complex Element of COMPLEX
n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
v is complex Element of COMPLEX
v " is complex Element of COMPLEX
t is complex Element of COMPLEX
t " is complex Element of COMPLEX
n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x * n is complex Element of the carrier of ()
the multF of () . (x,n) is complex Element of the carrier of ()
[x,n] is set
the multF of () . [x,n] is set
x * n is complex Element of COMPLEX
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
t is complex Element of COMPLEX
t " is complex Element of COMPLEX
v is complex Element of COMPLEX
v * t is complex Element of COMPLEX
t is complex Element of COMPLEX
t " is complex Element of COMPLEX
v is complex Element of COMPLEX
t * v is complex Element of COMPLEX
n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x * n is complex Element of the carrier of ()
the multF of () . (x,n) is complex Element of the carrier of ()
[x,n] is set
the multF of () . [x,n] is set
x * n is complex Element of COMPLEX
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
v is complex Element of the carrier of ()
v * (n ") is complex Element of the carrier of ()
the multF of () . (v,(n ")) is complex Element of the carrier of ()
[v,(n ")] is set
the multF of () . [v,(n ")] is set
v * (n ") is complex Element of COMPLEX
(n ") * v is complex Element of the carrier of ()
the multF of () . ((n "),v) is complex Element of the carrier of ()
[(n "),v] is set
the multF of () . [(n "),v] is set
(n ") * v is complex Element of COMPLEX
t is complex Element of COMPLEX
t " is complex Element of COMPLEX
(1. ()) " is complex Element of the carrier of ()
1r " is complex Element of COMPLEX
n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
(n * x) " is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
(n ") * (x ") is complex Element of the carrier of ()
the multF of () . ((n "),(x ")) is complex Element of the carrier of ()
[(n "),(x ")] is set
the multF of () . [(n "),(x ")] is set
(n ") * (x ") is complex Element of COMPLEX
v is complex Element of COMPLEX
v " is complex Element of COMPLEX
t is complex Element of COMPLEX
t " is complex Element of COMPLEX
v * t is complex Element of COMPLEX
(v * t) " is complex Element of COMPLEX
n is complex Element of the carrier of ()
- n is complex Element of the carrier of ()
(- n) " is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
- (n ") is complex Element of the carrier of ()
x is complex Element of COMPLEX
- x is complex Element of COMPLEX
x " is complex Element of COMPLEX
(- x) " is complex Element of COMPLEX
- (x ") is complex Element of COMPLEX
n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
(n ") + (x ") is complex Element of the carrier of ()
the addF of () . ((n "),(x ")) is complex Element of the carrier of ()
[(n "),(x ")] is set
the addF of () . [(n "),(x ")] is set
(n ") + (x ") is complex Element of COMPLEX
n + x is complex Element of the carrier of ()
the addF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the addF of () . [n,x] is set
n + x is complex Element of COMPLEX
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
(n * x) " is complex Element of the carrier of ()
(n + x) * ((n * x) ") is complex Element of the carrier of ()
the multF of () . ((n + x),((n * x) ")) is complex Element of the carrier of ()
[(n + x),((n * x) ")] is set
the multF of () . [(n + x),((n * x) ")] is set
(n + x) * ((n * x) ") is complex Element of COMPLEX
v is complex Element of COMPLEX
v " is complex Element of COMPLEX
t is complex Element of COMPLEX
v * t is complex Element of COMPLEX
(v * t) " is complex Element of COMPLEX
t " is complex Element of COMPLEX
n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
(n ") - (x ") is complex Element of the carrier of ()
- (x ") is complex Element of the carrier of ()
(n ") + (- (x ")) is complex Element of the carrier of ()
the addF of () . ((n "),(- (x "))) is complex Element of the carrier of ()
[(n "),(- (x "))] is set
the addF of () . [(n "),(- (x "))] is set
(n ") + (- (x ")) is complex Element of COMPLEX
x - n is complex Element of the carrier of ()
- n is complex Element of the carrier of ()
x + (- n) is complex Element of the carrier of ()
the addF of () . (x,(- n)) is complex Element of the carrier of ()
[x,(- n)] is set
the addF of () . [x,(- n)] is set
x + (- n) is complex Element of COMPLEX
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
(n * x) " is complex Element of the carrier of ()
(x - n) * ((n * x) ") is complex Element of the carrier of ()
the multF of () . ((x - n),((n * x) ")) is complex Element of the carrier of ()
[(x - n),((n * x) ")] is set
the multF of () . [(x - n),((n * x) ")] is set
(x - n) * ((n * x) ") is complex Element of COMPLEX
t is complex Element of COMPLEX
v is complex Element of COMPLEX
t - v is complex Element of COMPLEX
v " is complex Element of COMPLEX
v * t is complex Element of COMPLEX
(v * t) " is complex Element of COMPLEX
t " is complex Element of COMPLEX
(v ") - (t ") is complex Element of COMPLEX
n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
(1. ()) / n is complex Element of the carrier of ()
(1. ()) * (n ") is complex Element of the carrier of ()
the multF of () . ((1. ()),(n ")) is complex Element of the carrier of ()
[(1. ()),(n ")] is set
the multF of () . [(1. ()),(n ")] is set
(1. ()) * (n ") is complex Element of COMPLEX
x is complex Element of COMPLEX
x " is complex Element of COMPLEX
1r / x is complex Element of COMPLEX
n is complex Element of the carrier of ()
n / (1. ()) is complex Element of the carrier of ()
n * ((1. ()) ") is complex Element of the carrier of ()
the multF of () . (n,((1. ()) ")) is complex Element of the carrier of ()
[n,((1. ()) ")] is set
the multF of () . [n,((1. ()) ")] is set
n * ((1. ()) ") is complex Element of COMPLEX
x is complex Element of COMPLEX
x / 1r is complex Element of COMPLEX
n is complex Element of the carrier of ()
n / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
n * (n ") is complex Element of the carrier of ()
the multF of () . (n,(n ")) is complex Element of the carrier of ()
[n,(n ")] is set
the multF of () . [n,(n ")] is set
n * (n ") is complex Element of COMPLEX
x is complex Element of COMPLEX
x / x is complex Element of COMPLEX
n is complex Element of the carrier of ()
(0. ()) / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
(0. ()) * (n ") is complex Element of the carrier of ()
the multF of () . ((0. ()),(n ")) is complex Element of the carrier of ()
[(0. ()),(n ")] is set
the multF of () . [(0. ()),(n ")] is set
(0. ()) * (n ") is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x * (n ") is complex Element of the carrier of ()
the multF of () . (x,(n ")) is complex Element of the carrier of ()
[x,(n ")] is set
the multF of () . [x,(n ")] is set
x * (n ") is complex Element of COMPLEX
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v / t is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
v is complex Element of the carrier of ()
v / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
v * (n ") is complex Element of the carrier of ()
the multF of () . (v,(n ")) is complex Element of the carrier of ()
[v,(n ")] is set
the multF of () . [v,(n ")] is set
v * (n ") is complex Element of COMPLEX
t is complex Element of the carrier of ()
t / x is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
t * (x ") is complex Element of the carrier of ()
the multF of () . (t,(x ")) is complex Element of the carrier of ()
[t,(x ")] is set
the multF of () . [t,(x ")] is set
t * (x ") is complex Element of COMPLEX
(v / n) * (t / x) is complex Element of the carrier of ()
the multF of () . ((v / n),(t / x)) is complex Element of the carrier of ()
[(v / n),(t / x)] is set
the multF of () . [(v / n),(t / x)] is set
(v / n) * (t / x) is complex Element of COMPLEX
v * t is complex Element of the carrier of ()
the multF of () . (v,t) is complex Element of the carrier of ()
[v,t] is set
the multF of () . [v,t] is set
v * t is complex Element of COMPLEX
(v * t) / (n * x) is complex Element of the carrier of ()
(n * x) " is complex Element of the carrier of ()
(v * t) * ((n * x) ") is complex Element of the carrier of ()
the multF of () . ((v * t),((n * x) ")) is complex Element of the carrier of ()
[(v * t),((n * x) ")] is set
the multF of () . [(v * t),((n * x) ")] is set
(v * t) * ((n * x) ") is complex Element of COMPLEX
t is complex Element of COMPLEX
z49 is complex Element of COMPLEX
t / z49 is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
t / t is complex Element of COMPLEX
t * t is complex Element of COMPLEX
t * z49 is complex Element of COMPLEX
(t * t) / (t * z49) is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
v is complex Element of the carrier of ()
v / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
v * (n ") is complex Element of the carrier of ()
the multF of () . (v,(n ")) is complex Element of the carrier of ()
[v,(n ")] is set
the multF of () . [v,(n ")] is set
v * (n ") is complex Element of COMPLEX
x * (v / n) is complex Element of the carrier of ()
the multF of () . (x,(v / n)) is complex Element of the carrier of ()
[x,(v / n)] is set
the multF of () . [x,(v / n)] is set
x * (v / n) is complex Element of COMPLEX
x * v is complex Element of the carrier of ()
the multF of () . (x,v) is complex Element of the carrier of ()
[x,v] is set
the multF of () . [x,v] is set
x * v is complex Element of COMPLEX
(x * v) / n is complex Element of the carrier of ()
(x * v) * (n ") is complex Element of the carrier of ()
the multF of () . ((x * v),(n ")) is complex Element of the carrier of ()
[(x * v),(n ")] is set
the multF of () . [(x * v),(n ")] is set
(x * v) * (n ") is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x * (n ") is complex Element of the carrier of ()
the multF of () . (x,(n ")) is complex Element of the carrier of ()
[x,(n ")] is set
the multF of () . [x,(n ")] is set
x * (n ") is complex Element of COMPLEX
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v / t is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x * n is complex Element of the carrier of ()
the multF of () . (x,n) is complex Element of the carrier of ()
[x,n] is set
the multF of () . [x,n] is set
x * n is complex Element of COMPLEX
(x * n) / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
(x * n) * (n ") is complex Element of the carrier of ()
the multF of () . ((x * n),(n ")) is complex Element of the carrier of ()
[(x * n),(n ")] is set
the multF of () . [(x * n),(n ")] is set
(x * n) * (n ") is complex Element of COMPLEX
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v * t is complex Element of COMPLEX
(v * t) / t is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n / x is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
n * (x ") is complex Element of the carrier of ()
the multF of () . (n,(x ")) is complex Element of the carrier of ()
[n,(x ")] is set
the multF of () . [n,(x ")] is set
n * (x ") is complex Element of COMPLEX
(n / x) " is complex Element of the carrier of ()
x / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x * (n ") is complex Element of the carrier of ()
the multF of () . (x,(n ")) is complex Element of the carrier of ()
[x,(n ")] is set
the multF of () . [x,(n ")] is set
x * (n ") is complex Element of COMPLEX
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v / t is complex Element of COMPLEX
(v / t) " is complex Element of COMPLEX
t / v is complex Element of COMPLEX
n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
(n ") / (x ") is complex Element of the carrier of ()
(x ") " is complex Element of the carrier of ()
(n ") * ((x ") ") is complex Element of the carrier of ()
the multF of () . ((n "),((x ") ")) is complex Element of the carrier of ()
[(n "),((x ") ")] is set
the multF of () . [(n "),((x ") ")] is set
(n ") * ((x ") ") is complex Element of COMPLEX
x / n is complex Element of the carrier of ()
x * (n ") is complex Element of the carrier of ()
the multF of () . (x,(n ")) is complex Element of the carrier of ()
[x,(n ")] is set
the multF of () . [x,(n ")] is set
x * (n ") is complex Element of COMPLEX
t is complex Element of COMPLEX
t " is complex Element of COMPLEX
v is complex Element of COMPLEX
v " is complex Element of COMPLEX
(v ") / (t ") is complex Element of COMPLEX
t / v is complex Element of COMPLEX
n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x / (n ") is complex Element of the carrier of ()
(n ") " is complex Element of the carrier of ()
x * ((n ") ") is complex Element of the carrier of ()
the multF of () . (x,((n ") ")) is complex Element of the carrier of ()
[x,((n ") ")] is set
the multF of () . [x,((n ") ")] is set
x * ((n ") ") is complex Element of COMPLEX
x * n is complex Element of the carrier of ()
the multF of () . (x,n) is complex Element of the carrier of ()
[x,n] is set
the multF of () . [x,n] is set
x * n is complex Element of COMPLEX
t is complex Element of COMPLEX
t " is complex Element of COMPLEX
v is complex Element of COMPLEX
v / (t ") is complex Element of COMPLEX
n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x is complex Element of the carrier of ()
(n ") / x is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
(n ") * (x ") is complex Element of the carrier of ()
the multF of () . ((n "),(x ")) is complex Element of the carrier of ()
[(n "),(x ")] is set
the multF of () . [(n "),(x ")] is set
(n ") * (x ") is complex Element of COMPLEX
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
(n * x) " is complex Element of the carrier of ()
v is complex Element of COMPLEX
v " is complex Element of COMPLEX
t is complex Element of COMPLEX
(v ") / t is complex Element of COMPLEX
v * t is complex Element of COMPLEX
(v * t) " is complex Element of COMPLEX
n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
v is complex Element of the carrier of ()
v / x is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
v * (x ") is complex Element of the carrier of ()
the multF of () . (v,(x ")) is complex Element of the carrier of ()
[v,(x ")] is set
the multF of () . [v,(x ")] is set
v * (x ") is complex Element of COMPLEX
(n ") * (v / x) is complex Element of the carrier of ()
the multF of () . ((n "),(v / x)) is complex Element of the carrier of ()
[(n "),(v / x)] is set
the multF of () . [(n "),(v / x)] is set
(n ") * (v / x) is complex Element of COMPLEX
v / (n * x) is complex Element of the carrier of ()
(n * x) " is complex Element of the carrier of ()
v * ((n * x) ") is complex Element of the carrier of ()
the multF of () . (v,((n * x) ")) is complex Element of the carrier of ()
[v,((n * x) ")] is set
the multF of () . [v,((n * x) ")] is set
v * ((n * x) ") is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
t / t is complex Element of COMPLEX
t is complex Element of COMPLEX
t " is complex Element of COMPLEX
t * t is complex Element of COMPLEX
t / (t * t) is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x * n is complex Element of the carrier of ()
the multF of () . (x,n) is complex Element of the carrier of ()
[x,n] is set
the multF of () . [x,n] is set
x * n is complex Element of COMPLEX
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
v is complex Element of the carrier of ()
v / x is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
v * (x ") is complex Element of the carrier of ()
the multF of () . (v,(x ")) is complex Element of the carrier of ()
[v,(x ")] is set
the multF of () . [v,(x ")] is set
v * (x ") is complex Element of COMPLEX
v * n is complex Element of the carrier of ()
the multF of () . (v,n) is complex Element of the carrier of ()
[v,n] is set
the multF of () . [v,n] is set
v * n is complex Element of COMPLEX
(v * n) / (x * n) is complex Element of the carrier of ()
(x * n) " is complex Element of the carrier of ()
(v * n) * ((x * n) ") is complex Element of the carrier of ()
the multF of () . ((v * n),((x * n) ")) is complex Element of the carrier of ()
[(v * n),((x * n) ")] is set
the multF of () . [(v * n),((x * n) ")] is set
(v * n) * ((x * n) ") is complex Element of COMPLEX
n * v is complex Element of the carrier of ()
the multF of () . (n,v) is complex Element of the carrier of ()
[n,v] is set
the multF of () . [n,v] is set
n * v is complex Element of COMPLEX
(n * v) / (n * x) is complex Element of the carrier of ()
(n * x) " is complex Element of the carrier of ()
(n * v) * ((n * x) ") is complex Element of the carrier of ()
the multF of () . ((n * v),((n * x) ")) is complex Element of the carrier of ()
[(n * v),((n * x) ")] is set
the multF of () . [(n * v),((n * x) ")] is set
(n * v) * ((n * x) ") is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
t / t is complex Element of COMPLEX
t is complex Element of COMPLEX
t * t is complex Element of COMPLEX
t * t is complex Element of COMPLEX
(t * t) / (t * t) is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
v is complex Element of the carrier of ()
v / (n * x) is complex Element of the carrier of ()
(n * x) " is complex Element of the carrier of ()
v * ((n * x) ") is complex Element of the carrier of ()
the multF of () . (v,((n * x) ")) is complex Element of the carrier of ()
[v,((n * x) ")] is set
the multF of () . [v,((n * x) ")] is set
v * ((n * x) ") is complex Element of COMPLEX
v / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
v * (n ") is complex Element of the carrier of ()
the multF of () . (v,(n ")) is complex Element of the carrier of ()
[v,(n ")] is set
the multF of () . [v,(n ")] is set
v * (n ") is complex Element of COMPLEX
(v / n) / x is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
(v / n) * (x ") is complex Element of the carrier of ()
the multF of () . ((v / n),(x ")) is complex Element of the carrier of ()
[(v / n),(x ")] is set
the multF of () . [(v / n),(x ")] is set
(v / n) * (x ") is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
t / t is complex Element of COMPLEX
t is complex Element of COMPLEX
t * t is complex Element of COMPLEX
t / (t * t) is complex Element of COMPLEX
(t / t) / t is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n / x is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
n * (x ") is complex Element of the carrier of ()
the multF of () . (n,(x ")) is complex Element of the carrier of ()
[n,(x ")] is set
the multF of () . [n,(x ")] is set
n * (x ") is complex Element of COMPLEX
v is complex Element of the carrier of ()
v * x is complex Element of the carrier of ()
the multF of () . (v,x) is complex Element of the carrier of ()
[v,x] is set
the multF of () . [v,x] is set
v * x is complex Element of COMPLEX
(v * x) / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
(v * x) * (n ") is complex Element of the carrier of ()
the multF of () . ((v * x),(n ")) is complex Element of the carrier of ()
[(v * x),(n ")] is set
the multF of () . [(v * x),(n ")] is set
(v * x) * (n ") is complex Element of COMPLEX
v / (n / x) is complex Element of the carrier of ()
(n / x) " is complex Element of the carrier of ()
v * ((n / x) ") is complex Element of the carrier of ()
the multF of () . (v,((n / x) ")) is complex Element of the carrier of ()
[v,((n / x) ")] is set
the multF of () . [v,((n / x) ")] is set
v * ((n / x) ") is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
t / t is complex Element of COMPLEX
t is complex Element of COMPLEX
t * t is complex Element of COMPLEX
(t * t) / t is complex Element of COMPLEX
t / (t / t) is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
v is complex Element of the carrier of ()
x / v is complex Element of the carrier of ()
v " is complex Element of the carrier of ()
x * (v ") is complex Element of the carrier of ()
the multF of () . (x,(v ")) is complex Element of the carrier of ()
[x,(v ")] is set
the multF of () . [x,(v ")] is set
x * (v ") is complex Element of COMPLEX
t is complex Element of the carrier of ()
t / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
t * (n ") is complex Element of the carrier of ()
the multF of () . (t,(n ")) is complex Element of the carrier of ()
[t,(n ")] is set
the multF of () . [t,(n ")] is set
t * (n ") is complex Element of COMPLEX
(t / n) / (x / v) is complex Element of the carrier of ()
(x / v) " is complex Element of the carrier of ()
(t / n) * ((x / v) ") is complex Element of the carrier of ()
the multF of () . ((t / n),((x / v) ")) is complex Element of the carrier of ()
[(t / n),((x / v) ")] is set
the multF of () . [(t / n),((x / v) ")] is set
(t / n) * ((x / v) ") is complex Element of COMPLEX
t * v is complex Element of the carrier of ()
the multF of () . (t,v) is complex Element of the carrier of ()
[t,v] is set
the multF of () . [t,v] is set
t * v is complex Element of COMPLEX
(t * v) / (n * x) is complex Element of the carrier of ()
(n * x) " is complex Element of the carrier of ()
(t * v) * ((n * x) ") is complex Element of the carrier of ()
the multF of () . ((t * v),((n * x) ")) is complex Element of the carrier of ()
[(t * v),((n * x) ")] is set
the multF of () . [(t * v),((n * x) ")] is set
(t * v) * ((n * x) ") is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
t / t is complex Element of COMPLEX
t is complex Element of COMPLEX
z49 is complex Element of COMPLEX
t / z49 is complex Element of COMPLEX
(t / t) / (t / z49) is complex Element of COMPLEX
t * z49 is complex Element of COMPLEX
t * t is complex Element of COMPLEX
(t * z49) / (t * t) is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
v is complex Element of the carrier of ()
v / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
v * (n ") is complex Element of the carrier of ()
the multF of () . (v,(n ")) is complex Element of the carrier of ()
[v,(n ")] is set
the multF of () . [v,(n ")] is set
v * (n ") is complex Element of COMPLEX
v * x is complex Element of the carrier of ()
the multF of () . (v,x) is complex Element of the carrier of ()
[v,x] is set
the multF of () . [v,x] is set
v * x is complex Element of COMPLEX
t is complex Element of the carrier of ()
t / x is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
t * (x ") is complex Element of the carrier of ()
the multF of () . (t,(x ")) is complex Element of the carrier of ()
[t,(x ")] is set
the multF of () . [t,(x ")] is set
t * (x ") is complex Element of COMPLEX
(v / n) + (t / x) is complex Element of the carrier of ()
the addF of () . ((v / n),(t / x)) is complex Element of the carrier of ()
[(v / n),(t / x)] is set
the addF of () . [(v / n),(t / x)] is set
(v / n) + (t / x) is complex Element of COMPLEX
t * n is complex Element of the carrier of ()
the multF of () . (t,n) is complex Element of the carrier of ()
[t,n] is set
the multF of () . [t,n] is set
t * n is complex Element of COMPLEX
(v * x) + (t * n) is complex Element of the carrier of ()
the addF of () . ((v * x),(t * n)) is complex Element of the carrier of ()
[(v * x),(t * n)] is set
the addF of () . [(v * x),(t * n)] is set
(v * x) + (t * n) is complex Element of COMPLEX
((v * x) + (t * n)) / (n * x) is complex Element of the carrier of ()
(n * x) " is complex Element of the carrier of ()
((v * x) + (t * n)) * ((n * x) ") is complex Element of the carrier of ()
the multF of () . (((v * x) + (t * n)),((n * x) ")) is complex Element of the carrier of ()
[((v * x) + (t * n)),((n * x) ")] is set
the multF of () . [((v * x) + (t * n)),((n * x) ")] is set
((v * x) + (t * n)) * ((n * x) ") is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
t / t is complex Element of COMPLEX
t is complex Element of COMPLEX
z49 is complex Element of COMPLEX
t / z49 is complex Element of COMPLEX
t * z49 is complex Element of COMPLEX
t * t is complex Element of COMPLEX
(t * z49) + (t * t) is complex Element of COMPLEX
t * z49 is complex Element of COMPLEX
((t * z49) + (t * t)) / (t * z49) is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x * (n ") is complex Element of the carrier of ()
the multF of () . (x,(n ")) is complex Element of the carrier of ()
[x,(n ")] is set
the multF of () . [x,(n ")] is set
x * (n ") is complex Element of COMPLEX
v is complex Element of the carrier of ()
v / n is complex Element of the carrier of ()
v * (n ") is complex Element of the carrier of ()
the multF of () . (v,(n ")) is complex Element of the carrier of ()
[v,(n ")] is set
the multF of () . [v,(n ")] is set
v * (n ") is complex Element of COMPLEX
(x / n) + (v / n) is complex Element of the carrier of ()
the addF of () . ((x / n),(v / n)) is complex Element of the carrier of ()
[(x / n),(v / n)] is set
the addF of () . [(x / n),(v / n)] is set
(x / n) + (v / n) is complex Element of COMPLEX
x + v is complex Element of the carrier of ()
the addF of () . (x,v) is complex Element of the carrier of ()
[x,v] is set
the addF of () . [x,v] is set
x + v is complex Element of COMPLEX
(x + v) / n is complex Element of the carrier of ()
(x + v) * (n ") is complex Element of the carrier of ()
the multF of () . ((x + v),(n ")) is complex Element of the carrier of ()
[(x + v),(n ")] is set
the multF of () . [(x + v),(n ")] is set
(x + v) * (n ") is complex Element of COMPLEX
n is complex Element of the carrier of ()
- n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x * (n ") is complex Element of the carrier of ()
the multF of () . (x,(n ")) is complex Element of the carrier of ()
[x,(n ")] is set
the multF of () . [x,(n ")] is set
x * (n ") is complex Element of COMPLEX
- (x / n) is complex Element of the carrier of ()
- x is complex Element of the carrier of ()
(- x) / n is complex Element of the carrier of ()
(- x) * (n ") is complex Element of the carrier of ()
the multF of () . ((- x),(n ")) is complex Element of the carrier of ()
[(- x),(n ")] is set
the multF of () . [(- x),(n ")] is set
(- x) * (n ") is complex Element of COMPLEX
x / (- n) is complex Element of the carrier of ()
(- n) " is complex Element of the carrier of ()
x * ((- n) ") is complex Element of the carrier of ()
the multF of () . (x,((- n) ")) is complex Element of the carrier of ()
[x,((- n) ")] is set
the multF of () . [x,((- n) ")] is set
x * ((- n) ") is complex Element of COMPLEX
v is complex Element of COMPLEX
- v is complex Element of COMPLEX
t is complex Element of COMPLEX
v / t is complex Element of COMPLEX
- (v / t) is complex Element of COMPLEX
(- v) / t is complex Element of COMPLEX
- t is complex Element of COMPLEX
v / (- t) is complex Element of COMPLEX
n is complex Element of the carrier of ()
- n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x * (n ") is complex Element of the carrier of ()
the multF of () . (x,(n ")) is complex Element of the carrier of ()
[x,(n ")] is set
the multF of () . [x,(n ")] is set
x * (n ") is complex Element of COMPLEX
- x is complex Element of the carrier of ()
(- x) / (- n) is complex Element of the carrier of ()
(- n) " is complex Element of the carrier of ()
(- x) * ((- n) ") is complex Element of the carrier of ()
the multF of () . ((- x),((- n) ")) is complex Element of the carrier of ()
[(- x),((- n) ")] is set
the multF of () . [(- x),((- n) ")] is set
(- x) * ((- n) ") is complex Element of COMPLEX
v is complex Element of COMPLEX
- v is complex Element of COMPLEX
t is complex Element of COMPLEX
- t is complex Element of COMPLEX
v / t is complex Element of COMPLEX
(- v) / (- t) is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
v is complex Element of the carrier of ()
v / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
v * (n ") is complex Element of the carrier of ()
the multF of () . (v,(n ")) is complex Element of the carrier of ()
[v,(n ")] is set
the multF of () . [v,(n ")] is set
v * (n ") is complex Element of COMPLEX
v * x is complex Element of the carrier of ()
the multF of () . (v,x) is complex Element of the carrier of ()
[v,x] is set
the multF of () . [v,x] is set
v * x is complex Element of COMPLEX
t is complex Element of the carrier of ()
t / x is complex Element of the carrier of ()
x " is complex Element of the carrier of ()
t * (x ") is complex Element of the carrier of ()
the multF of () . (t,(x ")) is complex Element of the carrier of ()
[t,(x ")] is set
the multF of () . [t,(x ")] is set
t * (x ") is complex Element of COMPLEX
(v / n) - (t / x) is complex Element of the carrier of ()
- (t / x) is complex Element of the carrier of ()
(v / n) + (- (t / x)) is complex Element of the carrier of ()
the addF of () . ((v / n),(- (t / x))) is complex Element of the carrier of ()
[(v / n),(- (t / x))] is set
the addF of () . [(v / n),(- (t / x))] is set
(v / n) + (- (t / x)) is complex Element of COMPLEX
t * n is complex Element of the carrier of ()
the multF of () . (t,n) is complex Element of the carrier of ()
[t,n] is set
the multF of () . [t,n] is set
t * n is complex Element of COMPLEX
(v * x) - (t * n) is complex Element of the carrier of ()
- (t * n) is complex Element of the carrier of ()
(v * x) + (- (t * n)) is complex Element of the carrier of ()
the addF of () . ((v * x),(- (t * n))) is complex Element of the carrier of ()
[(v * x),(- (t * n))] is set
the addF of () . [(v * x),(- (t * n))] is set
(v * x) + (- (t * n)) is complex Element of COMPLEX
((v * x) - (t * n)) / (n * x) is complex Element of the carrier of ()
(n * x) " is complex Element of the carrier of ()
((v * x) - (t * n)) * ((n * x) ") is complex Element of the carrier of ()
the multF of () . (((v * x) - (t * n)),((n * x) ")) is complex Element of the carrier of ()
[((v * x) - (t * n)),((n * x) ")] is set
the multF of () . [((v * x) - (t * n)),((n * x) ")] is set
((v * x) - (t * n)) * ((n * x) ") is complex Element of COMPLEX
t is complex Element of COMPLEX
z49 is complex Element of COMPLEX
t * z49 is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
t * t is complex Element of COMPLEX
(t * z49) - (t * t) is complex Element of COMPLEX
t / t is complex Element of COMPLEX
t / z49 is complex Element of COMPLEX
(t / t) - (t / z49) is complex Element of COMPLEX
t * z49 is complex Element of COMPLEX
((t * z49) - (t * t)) / (t * z49) is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x * (n ") is complex Element of the carrier of ()
the multF of () . (x,(n ")) is complex Element of the carrier of ()
[x,(n ")] is set
the multF of () . [x,(n ")] is set
x * (n ") is complex Element of COMPLEX
v is complex Element of the carrier of ()
v / n is complex Element of the carrier of ()
v * (n ") is complex Element of the carrier of ()
the multF of () . (v,(n ")) is complex Element of the carrier of ()
[v,(n ")] is set
the multF of () . [v,(n ")] is set
v * (n ") is complex Element of COMPLEX
(x / n) - (v / n) is complex Element of the carrier of ()
- (v / n) is complex Element of the carrier of ()
(x / n) + (- (v / n)) is complex Element of the carrier of ()
the addF of () . ((x / n),(- (v / n))) is complex Element of the carrier of ()
[(x / n),(- (v / n))] is set
the addF of () . [(x / n),(- (v / n))] is set
(x / n) + (- (v / n)) is complex Element of COMPLEX
x - v is complex Element of the carrier of ()
- v is complex Element of the carrier of ()
x + (- v) is complex Element of the carrier of ()
the addF of () . (x,(- v)) is complex Element of the carrier of ()
[x,(- v)] is set
the addF of () . [x,(- v)] is set
x + (- v) is complex Element of COMPLEX
(x - v) / n is complex Element of the carrier of ()
(x - v) * (n ") is complex Element of the carrier of ()
the multF of () . ((x - v),(n ")) is complex Element of the carrier of ()
[(x - v),(n ")] is set
the multF of () . [(x - v),(n ")] is set
(x - v) * (n ") is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
t - t is complex Element of COMPLEX
t is complex Element of COMPLEX
t / t is complex Element of COMPLEX
t / t is complex Element of COMPLEX
(t / t) - (t / t) is complex Element of COMPLEX
(t - t) / t is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
x * n is complex Element of the carrier of ()
the multF of () . (x,n) is complex Element of the carrier of ()
[x,n] is set
the multF of () . [x,n] is set
x * n is complex Element of COMPLEX
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
v is complex Element of the carrier of ()
v / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
v * (n ") is complex Element of the carrier of ()
the multF of () . (v,(n ")) is complex Element of the carrier of ()
[v,(n ")] is set
the multF of () . [v,(n ")] is set
v * (n ") is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
t / t is complex Element of COMPLEX
t is complex Element of COMPLEX
t is complex Element of COMPLEX
t / t is complex Element of COMPLEX
((0. ())) is complex Element of the carrier of ()
Re (0. ()) is ext-real complex V35() Element of REAL
Im (0. ()) is ext-real complex V35() Element of REAL
(Im (0. ())) * <i> is complex set
(Re (0. ())) - ((Im (0. ())) * <i>) is complex set
n is complex Element of the carrier of ()
(n) is complex Element of the carrier of ()
Re n is ext-real complex V35() Element of REAL
Im n is ext-real complex V35() Element of REAL
(Im n) * <i> is complex set
(Re n) - ((Im n) * <i>) is complex set
((1. ())) is complex Element of the carrier of ()
Re (1. ()) is ext-real complex V35() Element of REAL
Im (1. ()) is ext-real complex V35() Element of REAL
(Im (1. ())) * <i> is complex set
(Re (1. ())) - ((Im (1. ())) * <i>) is complex set
n is complex Element of the carrier of ()
(n) is complex Element of the carrier of ()
Re n is ext-real complex V35() Element of REAL
Im n is ext-real complex V35() Element of REAL
(Im n) * <i> is complex set
(Re n) - ((Im n) * <i>) is complex set
((n)) is complex Element of the carrier of ()
Re (n) is ext-real complex V35() Element of REAL
Im (n) is ext-real complex V35() Element of REAL
(Im (n)) * <i> is complex set
(Re (n)) - ((Im (n)) * <i>) is complex set
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n + x is complex Element of the carrier of ()
the addF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the addF of () . [n,x] is set
n + x is complex Element of COMPLEX
((n + x)) is complex Element of the carrier of ()
Re (n + x) is ext-real complex V35() Element of REAL
Im (n + x) is ext-real complex V35() Element of REAL
(Im (n + x)) * <i> is complex set
(Re (n + x)) - ((Im (n + x)) * <i>) is complex set
(n) is complex Element of the carrier of ()
Re n is ext-real complex V35() Element of REAL
Im n is ext-real complex V35() Element of REAL
(Im n) * <i> is complex set
(Re n) - ((Im n) * <i>) is complex set
(x) is complex Element of the carrier of ()
Re x is ext-real complex V35() Element of REAL
Im x is ext-real complex V35() Element of REAL
(Im x) * <i> is complex set
(Re x) - ((Im x) * <i>) is complex set
(n) + (x) is complex Element of the carrier of ()
the addF of () . ((n),(x)) is complex Element of the carrier of ()
[(n),(x)] is set
the addF of () . [(n),(x)] is set
(n) + (x) is complex Element of COMPLEX
n is complex Element of the carrier of ()
- n is complex Element of the carrier of ()
((- n)) is complex Element of the carrier of ()
Re (- n) is ext-real complex V35() Element of REAL
Im (- n) is ext-real complex V35() Element of REAL
(Im (- n)) * <i> is complex set
(Re (- n)) - ((Im (- n)) * <i>) is complex set
(n) is complex Element of the carrier of ()
Re n is ext-real complex V35() Element of REAL
Im n is ext-real complex V35() Element of REAL
(Im n) * <i> is complex set
(Re n) - ((Im n) * <i>) is complex set
- (n) is complex Element of the carrier of ()
x is complex Element of COMPLEX
- x is complex Element of COMPLEX
x *' is complex Element of COMPLEX
Re x is ext-real complex V35() Element of REAL
Im x is ext-real complex V35() Element of REAL
(Im x) * <i> is complex set
(Re x) - ((Im x) * <i>) is complex set
- (x *') is complex Element of COMPLEX
n is complex Element of the carrier of ()
(n) is complex Element of the carrier of ()
Re n is ext-real complex V35() Element of REAL
Im n is ext-real complex V35() Element of REAL
(Im n) * <i> is complex set
(Re n) - ((Im n) * <i>) is complex set
x is complex Element of the carrier of ()
n - x is complex Element of the carrier of ()
- x is complex Element of the carrier of ()
n + (- x) is complex Element of the carrier of ()
the addF of () . (n,(- x)) is complex Element of the carrier of ()
[n,(- x)] is set
the addF of () . [n,(- x)] is set
n + (- x) is complex Element of COMPLEX
((n - x)) is complex Element of the carrier of ()
Re (n - x) is ext-real complex V35() Element of REAL
Im (n - x) is ext-real complex V35() Element of REAL
(Im (n - x)) * <i> is complex set
(Re (n - x)) - ((Im (n - x)) * <i>) is complex set
(x) is complex Element of the carrier of ()
Re x is ext-real complex V35() Element of REAL
Im x is ext-real complex V35() Element of REAL
(Im x) * <i> is complex set
(Re x) - ((Im x) * <i>) is complex set
(n) - (x) is complex Element of the carrier of ()
- (x) is complex Element of the carrier of ()
(n) + (- (x)) is complex Element of the carrier of ()
the addF of () . ((n),(- (x))) is complex Element of the carrier of ()
[(n),(- (x))] is set
the addF of () . [(n),(- (x))] is set
(n) + (- (x)) is complex Element of COMPLEX
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v - t is complex Element of COMPLEX
v *' is complex Element of COMPLEX
Re v is ext-real complex V35() Element of REAL
Im v is ext-real complex V35() Element of REAL
(Im v) * <i> is complex set
(Re v) - ((Im v) * <i>) is complex set
t *' is complex Element of COMPLEX
Re t is ext-real complex V35() Element of REAL
Im t is ext-real complex V35() Element of REAL
(Im t) * <i> is complex set
(Re t) - ((Im t) * <i>) is complex set
(v *') - (t *') is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
((n * x)) is complex Element of the carrier of ()
Re (n * x) is ext-real complex V35() Element of REAL
Im (n * x) is ext-real complex V35() Element of REAL
(Im (n * x)) * <i> is complex set
(Re (n * x)) - ((Im (n * x)) * <i>) is complex set
(n) is complex Element of the carrier of ()
Re n is ext-real complex V35() Element of REAL
Im n is ext-real complex V35() Element of REAL
(Im n) * <i> is complex set
(Re n) - ((Im n) * <i>) is complex set
(x) is complex Element of the carrier of ()
Re x is ext-real complex V35() Element of REAL
Im x is ext-real complex V35() Element of REAL
(Im x) * <i> is complex set
(Re x) - ((Im x) * <i>) is complex set
(n) * (x) is complex Element of the carrier of ()
the multF of () . ((n),(x)) is complex Element of the carrier of ()
[(n),(x)] is set
the multF of () . [(n),(x)] is set
(n) * (x) is complex Element of COMPLEX
n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
((n ")) is complex Element of the carrier of ()
Re (n ") is ext-real complex V35() Element of REAL
Im (n ") is ext-real complex V35() Element of REAL
(Im (n ")) * <i> is complex set
(Re (n ")) - ((Im (n ")) * <i>) is complex set
(n) is complex Element of the carrier of ()
Re n is ext-real complex V35() Element of REAL
Im n is ext-real complex V35() Element of REAL
(Im n) * <i> is complex set
(Re n) - ((Im n) * <i>) is complex set
(n) " is complex Element of the carrier of ()
x is complex Element of COMPLEX
x " is complex Element of COMPLEX
x *' is complex Element of COMPLEX
Re x is ext-real complex V35() Element of REAL
Im x is ext-real complex V35() Element of REAL
(Im x) * <i> is complex set
(Re x) - ((Im x) * <i>) is complex set
(x *') " is complex Element of COMPLEX
n is complex Element of the carrier of ()
(n) is complex Element of the carrier of ()
Re n is ext-real complex V35() Element of REAL
Im n is ext-real complex V35() Element of REAL
(Im n) * <i> is complex set
(Re n) - ((Im n) * <i>) is complex set
x is complex Element of the carrier of ()
x / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x * (n ") is complex Element of the carrier of ()
the multF of () . (x,(n ")) is complex Element of the carrier of ()
[x,(n ")] is set
the multF of () . [x,(n ")] is set
x * (n ") is complex Element of COMPLEX
((x / n)) is complex Element of the carrier of ()
Re (x / n) is ext-real complex V35() Element of REAL
Im (x / n) is ext-real complex V35() Element of REAL
(Im (x / n)) * <i> is complex set
(Re (x / n)) - ((Im (x / n)) * <i>) is complex set
(x) is complex Element of the carrier of ()
Re x is ext-real complex V35() Element of REAL
Im x is ext-real complex V35() Element of REAL
(Im x) * <i> is complex set
(Re x) - ((Im x) * <i>) is complex set
(x) / (n) is complex Element of the carrier of ()
(n) " is complex Element of the carrier of ()
(x) * ((n) ") is complex Element of the carrier of ()
the multF of () . ((x),((n) ")) is complex Element of the carrier of ()
[(x),((n) ")] is set
the multF of () . [(x),((n) ")] is set
(x) * ((n) ") is complex Element of COMPLEX
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v / t is complex Element of COMPLEX
v *' is complex Element of COMPLEX
Re v is ext-real complex V35() Element of REAL
Im v is ext-real complex V35() Element of REAL
(Im v) * <i> is complex set
(Re v) - ((Im v) * <i>) is complex set
t *' is complex Element of COMPLEX
Re t is ext-real complex V35() Element of REAL
Im t is ext-real complex V35() Element of REAL
(Im t) * <i> is complex set
(Re t) - ((Im t) * <i>) is complex set
(v *') / (t *') is complex Element of COMPLEX
|.(0. ()).| is ext-real non negative complex V35() Element of REAL
n is complex Element of the carrier of ()
|.n.| is ext-real non negative complex V35() Element of REAL
n is complex Element of the carrier of ()
|.n.| is ext-real non negative complex V35() Element of REAL
x is complex Element of the carrier of ()
|.x.| is ext-real non negative complex V35() Element of REAL
|.(1. ()).| is ext-real non negative complex V35() Element of REAL
n is complex Element of the carrier of ()
- n is complex Element of the carrier of ()
|.(- n).| is ext-real non negative complex V35() Element of REAL
|.n.| is ext-real non negative complex V35() Element of REAL
x is complex Element of COMPLEX
- x is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n + x is complex Element of the carrier of ()
the addF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the addF of () . [n,x] is set
n + x is complex Element of COMPLEX
|.(n + x).| is ext-real non negative complex V35() Element of REAL
|.n.| is ext-real non negative complex V35() Element of REAL
|.x.| is ext-real non negative complex V35() Element of REAL
|.n.| + |.x.| is ext-real non negative complex V35() Element of REAL
n is complex Element of the carrier of ()
|.n.| is ext-real non negative complex V35() Element of REAL
x is complex Element of the carrier of ()
n - x is complex Element of the carrier of ()
- x is complex Element of the carrier of ()
n + (- x) is complex Element of the carrier of ()
the addF of () . (n,(- x)) is complex Element of the carrier of ()
[n,(- x)] is set
the addF of () . [n,(- x)] is set
n + (- x) is complex Element of COMPLEX
|.(n - x).| is ext-real non negative complex V35() Element of REAL
|.x.| is ext-real non negative complex V35() Element of REAL
|.n.| + |.x.| is ext-real non negative complex V35() Element of REAL
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v - t is complex Element of COMPLEX
n is complex Element of the carrier of ()
|.n.| is ext-real non negative complex V35() Element of REAL
x is complex Element of the carrier of ()
|.x.| is ext-real non negative complex V35() Element of REAL
|.n.| - |.x.| is ext-real complex V35() Element of REAL
n + x is complex Element of the carrier of ()
the addF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the addF of () . [n,x] is set
n + x is complex Element of COMPLEX
|.(n + x).| is ext-real non negative complex V35() Element of REAL
n is complex Element of the carrier of ()
|.n.| is ext-real non negative complex V35() Element of REAL
x is complex Element of the carrier of ()
|.x.| is ext-real non negative complex V35() Element of REAL
|.n.| - |.x.| is ext-real complex V35() Element of REAL
n - x is complex Element of the carrier of ()
- x is complex Element of the carrier of ()
n + (- x) is complex Element of the carrier of ()
the addF of () . (n,(- x)) is complex Element of the carrier of ()
[n,(- x)] is set
the addF of () . [n,(- x)] is set
n + (- x) is complex Element of COMPLEX
|.(n - x).| is ext-real non negative complex V35() Element of REAL
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v - t is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n - x is complex Element of the carrier of ()
- x is complex Element of the carrier of ()
n + (- x) is complex Element of the carrier of ()
the addF of () . (n,(- x)) is complex Element of the carrier of ()
[n,(- x)] is set
the addF of () . [n,(- x)] is set
n + (- x) is complex Element of COMPLEX
|.(n - x).| is ext-real non negative complex V35() Element of REAL
x - n is complex Element of the carrier of ()
- n is complex Element of the carrier of ()
x + (- n) is complex Element of the carrier of ()
the addF of () . (x,(- n)) is complex Element of the carrier of ()
[x,(- n)] is set
the addF of () . [x,(- n)] is set
x + (- n) is complex Element of COMPLEX
|.(x - n).| is ext-real non negative complex V35() Element of REAL
t is complex Element of COMPLEX
v is complex Element of COMPLEX
t - v is complex Element of COMPLEX
v - t is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n - x is complex Element of the carrier of ()
- x is complex Element of the carrier of ()
n + (- x) is complex Element of the carrier of ()
the addF of () . (n,(- x)) is complex Element of the carrier of ()
[n,(- x)] is set
the addF of () . [n,(- x)] is set
n + (- x) is complex Element of COMPLEX
|.(n - x).| is ext-real non negative complex V35() Element of REAL
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v - t is complex Element of COMPLEX
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v - t is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n - x is complex Element of the carrier of ()
- x is complex Element of the carrier of ()
n + (- x) is complex Element of the carrier of ()
the addF of () . (n,(- x)) is complex Element of the carrier of ()
[n,(- x)] is set
the addF of () . [n,(- x)] is set
n + (- x) is complex Element of COMPLEX
|.(n - x).| is ext-real non negative complex V35() Element of REAL
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v - t is complex Element of COMPLEX
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v - t is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n - x is complex Element of the carrier of ()
- x is complex Element of the carrier of ()
n + (- x) is complex Element of the carrier of ()
the addF of () . (n,(- x)) is complex Element of the carrier of ()
[n,(- x)] is set
the addF of () . [n,(- x)] is set
n + (- x) is complex Element of COMPLEX
|.(n - x).| is ext-real non negative complex V35() Element of REAL
v is complex Element of the carrier of ()
n - v is complex Element of the carrier of ()
- v is complex Element of the carrier of ()
n + (- v) is complex Element of the carrier of ()
the addF of () . (n,(- v)) is complex Element of the carrier of ()
[n,(- v)] is set
the addF of () . [n,(- v)] is set
n + (- v) is complex Element of COMPLEX
|.(n - v).| is ext-real non negative complex V35() Element of REAL
v - x is complex Element of the carrier of ()
v + (- x) is complex Element of the carrier of ()
the addF of () . (v,(- x)) is complex Element of the carrier of ()
[v,(- x)] is set
the addF of () . [v,(- x)] is set
v + (- x) is complex Element of COMPLEX
|.(v - x).| is ext-real non negative complex V35() Element of REAL
|.(n - v).| + |.(v - x).| is ext-real non negative complex V35() Element of REAL
t is complex Element of COMPLEX
t is complex Element of COMPLEX
t - t is complex Element of COMPLEX
t is complex Element of COMPLEX
t - t is complex Element of COMPLEX
|.(t - t).| is ext-real non negative complex V35() Element of REAL
t - t is complex Element of COMPLEX
|.(t - t).| is ext-real non negative complex V35() Element of REAL
n is complex Element of the carrier of ()
|.n.| is ext-real non negative complex V35() Element of REAL
x is complex Element of the carrier of ()
|.x.| is ext-real non negative complex V35() Element of REAL
|.n.| - |.x.| is ext-real complex V35() Element of REAL
abs (|.n.| - |.x.|) is ext-real non negative complex V35() Element of REAL
n - x is complex Element of the carrier of ()
- x is complex Element of the carrier of ()
n + (- x) is complex Element of the carrier of ()
the addF of () . (n,(- x)) is complex Element of the carrier of ()
[n,(- x)] is set
the addF of () . [n,(- x)] is set
n + (- x) is complex Element of COMPLEX
|.(n - x).| is ext-real non negative complex V35() Element of REAL
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v - t is complex Element of COMPLEX
n is complex Element of the carrier of ()
x is complex Element of the carrier of ()
n * x is complex Element of the carrier of ()
the multF of () . (n,x) is complex Element of the carrier of ()
[n,x] is set
the multF of () . [n,x] is set
n * x is complex Element of COMPLEX
|.(n * x).| is ext-real non negative complex V35() Element of REAL
|.n.| is ext-real non negative complex V35() Element of REAL
|.x.| is ext-real non negative complex V35() Element of REAL
|.n.| * |.x.| is ext-real non negative complex V35() Element of REAL
n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
|.(n ").| is ext-real non negative complex V35() Element of REAL
|.n.| is ext-real non negative complex V35() Element of REAL
|.n.| " is ext-real non negative complex V35() Element of REAL
x is complex Element of COMPLEX
x " is complex Element of COMPLEX
n is complex Element of the carrier of ()
|.n.| is ext-real non negative complex V35() Element of REAL
x is complex Element of the carrier of ()
|.x.| is ext-real non negative complex V35() Element of REAL
|.x.| / |.n.| is ext-real non negative complex V35() Element of REAL
x / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x * (n ") is complex Element of the carrier of ()
the multF of () . (x,(n ")) is complex Element of the carrier of ()
[x,(n ")] is set
the multF of () . [x,(n ")] is set
x * (n ") is complex Element of COMPLEX
|.(x / n).| is ext-real non negative complex V35() Element of REAL
v is complex Element of COMPLEX
t is complex Element of COMPLEX
v / t is complex Element of COMPLEX
n is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
n is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() set
x + 1 is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
0 + 1 is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
v is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
t is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
t is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() set
t + 1 is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
t is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() set
t + 1 is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() set
x + 1 is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
power () is V1() V4(K20( the carrier of (),NAT)) V5( the carrier of ()) Function-like V18(K20( the carrier of (),NAT), the carrier of ()) Element of K19(K20(K20( the carrier of (),NAT), the carrier of ()))
K20( the carrier of (),NAT) is set
K20(K20( the carrier of (),NAT), the carrier of ()) is set
K19(K20(K20( the carrier of (),NAT), the carrier of ())) is set
n is complex Element of the carrier of ()
x is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() set
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
(power ()) . (n,v) is complex Element of the carrier of ()
[n,v] is set
(power ()) . [n,v] is set
(power ()) . (n,x) is set
[n,x] is set
(power ()) . [n,x] is set
n |^ x is set
x + 1 is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
(power ()) . (n,(x + 1)) is complex Element of the carrier of ()
[n,(x + 1)] is set
(power ()) . [n,(x + 1)] is set
t is complex Element of the carrier of ()
t * n is complex Element of the carrier of ()
the multF of () . (t,n) is complex Element of the carrier of ()
[t,n] is set
the multF of () . [t,n] is set
t * n is complex Element of COMPLEX
n |^ (x + 1) is set
(power ()) . (n,(x + 1)) is set
(power ()) . (n,1) is complex Element of the carrier of ()
[n,1] is set
(power ()) . [n,1] is set
(power ()) . (n,1) is set
n |^ 1 is set
n is complex Element of the carrier of ()
x is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
v is complex CRoot of x,n
v is complex Element of the carrier of ()
(power ()) . (v,x) is complex Element of the carrier of ()
[v,x] is set
(power ()) . [v,x] is set
v |^ x is set
v |^ x is set
n is complex Element of the carrier of ()
x is complex (n,1)
(power ()) . (x,1) is complex Element of the carrier of ()
[x,1] is set
(power ()) . [x,1] is set
n is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
x is complex ( 0. (),n)
v is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
(power ()) . (x,v) is complex Element of the carrier of ()
[x,v] is set
(power ()) . [x,v] is set
t is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() set
t + 1 is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
t is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
t is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
t is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
(power ()) . (x,t) is complex Element of the carrier of ()
[x,t] is set
(power ()) . [x,t] is set
((power ()) . (x,t)) * x is complex Element of the carrier of ()
the multF of () . (((power ()) . (x,t)),x) is complex Element of the carrier of ()
[((power ()) . (x,t)),x] is set
the multF of () . [((power ()) . (x,t)),x] is set
((power ()) . (x,t)) * x is complex Element of COMPLEX
(power ()) . (x,n) is complex Element of the carrier of ()
[x,n] is set
(power ()) . [x,n] is set
(power ()) . (x,1) is complex Element of the carrier of ()
[x,1] is set
(power ()) . [x,1] is set
n is non empty ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V35() Element of NAT
x is complex Element of the carrier of ()
v is complex (x,n)
(power ()) . ((0. ()),n) is complex Element of the carrier of ()
[(0. ()),n] is set
(power ()) . [(0. ()),n] is set