:: COMPLFLD semantic presentation

REAL is non empty V39() set

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

K19(omega) is set
K19(NAT) is set

() * <i> is complex set
() - (() * <i>) is complex set

() * <i> is complex set
() - (() * <i>) is complex set

the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) is set
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 #)

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

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

addcomplex . (t,t) is complex Element of COMPLEX
[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

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,t] is set
the addF of () . [t,t] is set

[( the addF of () . [t,t]),t] is set
addcomplex . (t,t) is complex Element of COMPLEX
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
the addF of () . [t,t] is set
[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

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

n 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
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

the multF of () . (t,t) is set
[t,t] is set
the multF of () . [t,t] is set

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

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
multcomplex . (t,(addcomplex . (t,t))) is complex Element of COMPLEX
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
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 ()

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

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

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

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

(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

(Im n) * <i> is complex set
(Re n) - ((Im n) * <i>) is complex set

- (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

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

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 + 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 - 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 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 * 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 ()
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

(1. ()) " 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 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 * 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
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 * 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 ()
(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 - v 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 ()
(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

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

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 / 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 / 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

z49 is complex Element of COMPLEX
t / z49 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 / 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 * 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 / 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

(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

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 ") / 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 / 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 / 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 / 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 / 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 / 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 / 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 / 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 ()
x / n is complex Element of the carrier of ()
n " is complex Element of the carrier of ()
x * (