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