:: FUNCT_8 semantic presentation

K6(REAL) is set

K6(omega) is set
K6(NAT) is set

K7(1,1) is Relation-like RAT -valued INT -valued V36() V37() V38() V39() set

K6(K7(1,1)) is set
K7(K7(1,1),1) is Relation-like RAT -valued INT -valued V36() V37() V38() V39() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is Relation-like V36() V37() V38() set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is Relation-like V36() V37() V38() set
K7(K7(REAL,REAL),REAL) is Relation-like V36() V37() V38() set
K6(K7(K7(REAL,REAL),REAL)) is set

K7(2,2) is Relation-like RAT -valued INT -valued V36() V37() V38() V39() set
K7(K7(2,2),REAL) is Relation-like V36() V37() V38() set
K6(K7(K7(2,2),REAL)) is set
COMPLEX is non zero V48() complex-membered V143() set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is V161() L15()
the U1 of () is set

{0c,1} is non zero set

K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is Relation-like V36() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is Relation-like RAT -valued V36() V37() V38() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is Relation-like RAT -valued V36() V37() V38() set
K6(K7(K7(RAT,RAT),RAT)) is set

K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is Relation-like RAT -valued INT -valued V36() V37() V38() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is Relation-like RAT -valued INT -valued V36() V37() V38() V39() set
K7(K7(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V36() V37() V38() V39() set
K6(K7(K7(NAT,NAT),NAT)) is set
K7(NAT,REAL) is Relation-like V36() V37() V38() set
K6(K7(NAT,REAL)) is set
K7(NAT,COMPLEX) is Relation-like V36() set
K6(K7(NAT,COMPLEX)) is set

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

- 1 is non zero complex real ext-real non positive negative set

2 " is non zero complex real ext-real positive non negative set

- (PI / 2) is complex real ext-real Element of REAL
].(- (PI / 2)),(PI / 2).[ is complex-membered ext-real-membered real-membered Element of K6(REAL)

K6(COMPLEX) is set

B is complex set
- B is complex set

B is complex set
- B is complex set

B is complex set
- B is complex set

B is Relation-like () set
dom B is set

K7(B,x) is Relation-like V36() set
K6(K7(B,x)) is set

K7(B,x) is Relation-like V36() set
K6(K7(B,x)) is set

K7(B,x) is Relation-like V36() set
K6(K7(B,x)) is set
x is Relation-like B -defined x -valued Function-like V36() Element of K6(K7(B,x))
x is Relation-like B -defined x -valued Function-like V36() Element of K6(K7(B,x))

K7(x,x) is Relation-like V36() set
K6(K7(x,x)) is set

K7(B,x) is Relation-like V36() set
K6(K7(B,x)) is set

K7(B,x) is Relation-like V36() set
K6(K7(B,x)) is set

K7(B,x) is Relation-like V36() set
K6(K7(B,x)) is set
x is Relation-like B -defined x -valued Function-like V36() Element of K6(K7(B,x))
x is Relation-like B -defined x -valued Function-like V36() Element of K6(K7(B,x))

K7(x,x) is Relation-like V36() set
K6(K7(x,x)) is set
B is complex-membered () Element of K6(COMPLEX)

dom (x | B) is complex-membered Element of K6(B)
K6(B) is set

x . (- x) is complex real ext-real set

- (x . x) is complex real ext-real set
(x . x) + (x . (- x)) is complex real ext-real set

(x | B) . (- x) is complex real ext-real set
(x | B) . x is complex real ext-real set
- ((x | B) . x) is complex real ext-real set
(x | B) /. (- x) is complex real ext-real Element of REAL
x /. (- x) is complex real ext-real Element of REAL
x . (- x) is complex real ext-real set

- (x . x) is complex real ext-real set

- (x /. x) is complex real ext-real Element of REAL
(x | B) /. x is complex real ext-real Element of REAL
- ((x | B) /. x) is complex real ext-real Element of REAL

x . (- x) is complex real ext-real set
(x . x) + (x . (- x)) is complex real ext-real set
dom (x | B) is complex-membered Element of K6(B)
K6(B) is set

(x /. x) + (x . (- x)) is complex real ext-real Element of REAL
x /. (- x) is complex real ext-real Element of REAL
(x /. x) + (x /. (- x)) is complex real ext-real Element of REAL
(x | B) /. x is complex real ext-real Element of REAL
((x | B) /. x) + (x /. (- x)) is complex real ext-real Element of REAL
(x | B) /. (- x) is complex real ext-real Element of REAL
((x | B) /. x) + ((x | B) /. (- x)) is complex real ext-real Element of REAL
(x | B) . (- x) is complex real ext-real set
((x | B) /. x) + ((x | B) . (- x)) is complex real ext-real Element of REAL
(x | B) . x is complex real ext-real set
((x | B) . x) + ((x | B) . (- x)) is complex real ext-real set
- ((x | B) . x) is complex real ext-real set
((x | B) . x) + (- ((x | B) . x)) is complex real ext-real set

x . (- x) is complex real ext-real set
(x . x) + (x . (- x)) is complex real ext-real set

x . (- x) is complex real ext-real set
(x . x) + (x . (- x)) is complex real ext-real set

x . (- x) is complex real ext-real set
(x . x) + (x . (- x)) is complex real ext-real set
B is complex-membered () Element of K6(COMPLEX)

dom (x | B) is complex-membered Element of K6(B)
K6(B) is set

x . (- x) is complex real ext-real set

(x . x) - (x . (- x)) is complex real ext-real set
- (x . (- x)) is complex real ext-real set
(x . x) + (- (x . (- x))) is complex real ext-real set

(x | B) . (- x) is complex real ext-real set
(x | B) . x is complex real ext-real set
(x | B) /. (- x) is complex real ext-real Element of REAL
x /. (- x) is complex real ext-real Element of REAL
x . (- x) is complex real ext-real set

(x | B) /. x is complex real ext-real Element of REAL

x . (- x) is complex real ext-real set
(x . x) - (x . (- x)) is complex real ext-real set
- (x . (- x)) is complex real ext-real set
(x . x) + (- (x . (- x))) is complex real ext-real set
dom (x | B) is complex-membered Element of K6(B)
K6(B) is set

(x /. x) - (x . (- x)) is complex real ext-real Element of REAL
(x /. x) + (- (x . (- x))) is complex real ext-real set
x /. (- x) is complex real ext-real Element of REAL
(x /. x) - (x /. (- x)) is complex real ext-real Element of REAL
- (x /. (- x)) is complex real ext-real set
(x /. x) + (- (x /. (- x))) is complex real ext-real set
(x | B) /. x is complex real ext-real Element of REAL
((x | B) /. x) - (x /. (- x)) is complex real ext-real Element of REAL
((x | B) /. x) + (- (x /. (- x))) is complex real ext-real set
(x | B) /. (- x) is complex real ext-real Element of REAL
((x | B) /. x) - ((x | B) /. (- x)) is complex real ext-real Element of REAL
- ((x | B) /. (- x)) is complex real ext-real set
((x | B) /. x) + (- ((x | B) /. (- x))) is complex real ext-real set
(x | B) . x is complex real ext-real set
((x | B) . x) - ((x | B) /. (- x)) is complex real ext-real Element of REAL
((x | B) . x) + (- ((x | B) /. (- x))) is complex real ext-real set
(x | B) . (- x) is complex real ext-real set
((x | B) . x) - ((x | B) . (- x)) is complex real ext-real set
- ((x | B) . (- x)) is complex real ext-real set
((x | B) . x) + (- ((x | B) . (- x))) is complex real ext-real set
((x | B) . x) - ((x | B) . x) is complex real ext-real set
- ((x | B) . x) is complex real ext-real set
((x | B) . x) + (- ((x | B) . x)) is complex real ext-real set

x . (- x) is complex real ext-real set
(x . x) - (x . (- x)) is complex real ext-real set
- (x . (- x)) is complex real ext-real set
(x . x) + (- (x . (- x))) is complex real ext-real set

x . (- x) is complex real ext-real set
(x . x) - (x . (- x)) is complex real ext-real set
- (x . (- x)) is complex real ext-real set
(x . x) + (- (x . (- x))) is complex real ext-real set

x . (- x) is complex real ext-real set
(x . x) - (x . (- x)) is complex real ext-real set
- (x . (- x)) is complex real ext-real set
(x . x) + (- (x . (- x))) is complex real ext-real set
B is complex-membered () Element of K6(COMPLEX)

x . (- x) is complex real ext-real set
(x . x) / (x . (- x)) is complex real ext-real set
(x . (- x)) " is complex real ext-real set
(x . x) * ((x . (- x)) ") is complex real ext-real set
dom (x | B) is complex-membered Element of K6(B)
K6(B) is set

(x | B) /. x is complex real ext-real Element of REAL
(x | B) . x is complex real ext-real set
(x /. x) / (x . (- x)) is complex real ext-real Element of REAL
(x /. x) * ((x . (- x)) ") is complex real ext-real set
x /. (- x) is complex real ext-real Element of REAL
(x /. x) / (x /. (- x)) is complex real ext-real Element of REAL
(x /. (- x)) " is complex real ext-real set
(x /. x) * ((x /. (- x)) ") is complex real ext-real set
((x | B) /. x) / (x /. (- x)) is complex real ext-real Element of REAL
((x | B) /. x) * ((x /. (- x)) ") is complex real ext-real set
(x | B) /. (- x) is complex real ext-real Element of REAL
((x | B) /. x) / ((x | B) /. (- x)) is complex real ext-real Element of REAL
((x | B) /. (- x)) " is complex real ext-real set
((x | B) /. x) * (((x | B) /. (- x)) ") is complex real ext-real set
((x | B) . x) / ((x | B) /. (- x)) is complex real ext-real Element of REAL
((x | B) . x) * (((x | B) /. (- x)) ") is complex real ext-real set
(x | B) . (- x) is complex real ext-real set
((x | B) . x) / ((x | B) . (- x)) is complex real ext-real set
((x | B) . (- x)) " is complex real ext-real set
((x | B) . x) * (((x | B) . (- x)) ") is complex real ext-real set
- ((x | B) . x) is complex real ext-real set
((x | B) . x) / (- ((x | B) . x)) is complex real ext-real set
(- ((x | B) . x)) " is complex real ext-real set
((x | B) . x) * ((- ((x | B) . x)) ") is complex real ext-real set
((x | B) . x) / ((x | B) . x) is complex real ext-real set
((x | B) . x) " is complex real ext-real set
((x | B) . x) * (((x | B) . x) ") is complex real ext-real set
- (((x | B) . x) / ((x | B) . x)) is complex real ext-real set

x . (- x) is complex real ext-real set
(x . x) / (x . (- x)) is complex real ext-real set
(x . (- x)) " is complex real ext-real set
(x . x) * ((x . (- x)) ") is complex real ext-real set
B is complex-membered () Element of K6(COMPLEX)

dom (x | B) is complex-membered Element of K6(B)
K6(B) is set

x . (- x) is complex real ext-real set

- (x . x) is complex real ext-real set
(x . x) / (x . (- x)) is complex real ext-real set
(x . (- x)) " is complex real ext-real set
(x . x) * ((x . (- x)) ") is complex real ext-real set

(x | B) . (- x) is complex real ext-real set
(x | B) . x is complex real ext-real set
- ((x | B) . x) is complex real ext-real set
(x | B) /. (- x) is complex real ext-real Element of REAL
x /. (- x) is complex real ext-real Element of REAL
x . (- x) is complex real ext-real set

- (x . x) is complex real ext-real set

- (x /. x) is complex real ext-real Element of REAL
(x | B) /. x is complex real ext-real Element of REAL
- ((x | B) /. x) is complex real ext-real Element of REAL
B is complex-membered () Element of K6(COMPLEX)

x . (- x) is complex real ext-real set
(x . x) / (x . (- x)) is complex real ext-real set
(x . (- x)) " is complex real ext-real set
(x . x) * ((x . (- x)) ") is complex real ext-real set
dom (x | B) is complex-membered Element of K6(B)
K6(B) is set

(x | B) /. x is complex real ext-real Element of REAL
(x | B) . x is complex real ext-real set
(x /. x) / (x . (- x)) is complex real ext-real Element of REAL
(x /. x) * ((x . (- x)) ") is complex real ext-real set
x /. (- x) is complex real ext-real Element of REAL
(x /. x) / (x /. (- x)) is complex real ext-real Element of REAL
(x /. (- x)) " is complex real ext-real set
(x /. x) * ((x /. (- x)) ") is complex real ext-real set
((x | B) /. x) / (x /. (- x)) is complex real ext-real Element of REAL
((x | B) /. x) * ((x /. (- x)) ") is complex real ext-real set
(x | B) /. (- x) is complex real ext-real Element of REAL
((x | B) /. x) / ((x | B) /. (- x)) is complex real ext-real Element of REAL
((x | B) /. (- x)) " is complex real ext-real set
((x | B) /. x) * (((x | B) /. (- x)) ") is complex real ext-real set
((x | B) . x) / ((x | B) /. (- x)) is complex real ext-real Element of REAL
((x | B) . x) * (((x | B) /. (- x)) ") is complex real ext-real set
(x | B) . (- x) is complex real ext-real set
((x | B) . x) / ((x | B) . (- x)) is complex real ext-real set
((x | B) . (- x)) " is complex real ext-real set
((x | B) . x) * (((x | B) . (- x)) ") is complex real ext-real set
((x | B) . x) / ((x | B) . x) is complex real ext-real set
((x | B) . x) " is complex real ext-real set
((x | B) . x) * (((x | B) . x) ") is complex real ext-real set

x . (- x) is complex real ext-real set
(x . x) / (x . (- x)) is complex real ext-real set
(x . (- x)) " is complex real ext-real set
(x . x) * ((x . (- x)) ") is complex real ext-real set
B is complex-membered () Element of K6(COMPLEX)

dom (x | B) is complex-membered Element of K6(B)
K6(B) is set

x . (- x) is complex real ext-real set

(x . x) / (x . (- x)) is complex real ext-real set
(x . (- x)) " is complex real ext-real set
(x . x) * ((x . (- x)) ") is complex real ext-real set

(x | B) . (- x) is complex real ext-real set
(x | B) . x is complex real ext-real set
(x | B) /. (- x) is complex real ext-real Element of REAL
x /. (- x) is complex real ext-real Element of REAL
x . (- x) is complex real ext-real set

(x | B) /. x is complex real ext-real Element of REAL
B is complex-membered () Element of K6(COMPLEX)

dom (x | B) is complex-membered Element of K6(B)
K6(B) is set

(x | B) /. x is complex real ext-real Element of REAL
(x | B) . x is complex real ext-real set
(x | B) . (- x) is complex real ext-real set
- ((x | B) . x) is complex real ext-real set
- ((x | B) /. x) is complex real ext-real Element of REAL
- (x /. x) is complex real ext-real Element of REAL
- (x . x) is complex real ext-real set
B is complex-membered () Element of K6(COMPLEX)

x . (abs x) is complex real ext-real set
dom (x | B) is complex-membered Element of K6(B)
K6(B) is set

x . (- x) is complex real ext-real set
x /. (- x) is complex real ext-real Element of REAL
(x | B) /. (- x) is complex real ext-real Element of REAL
(x | B) . (- x) is complex real ext-real set
(x | B) . x is complex real ext-real set
(x | B) /. x is complex real ext-real Element of REAL

B is complex-membered () Element of K6(COMPLEX)

dom (x | B) is complex-membered Element of K6(B)
K6(B) is set

x . (- x) is complex real ext-real set

x . (abs x) is complex real ext-real set

- (- x) is complex real ext-real Element of REAL

(x | B) . (- x) is complex real ext-real set
(x | B) . x is complex real ext-real set
(x | B) /. (- x) is complex real ext-real Element of REAL
x /. (- x) is complex real ext-real Element of REAL
x . (- x) is complex real ext-real set

(x | B) /. x is complex real ext-real Element of REAL
B is complex-membered () Element of K6(COMPLEX)

dom ((x + x) | B) is complex-membered Element of K6(B)
K6(B) is set

((x + x) | B) . (- x) is complex real ext-real set
((x + x) | B) . x is complex real ext-real set
- (((x + x) | B) . x) is complex real ext-real set
dom (x | B) is complex-membered Element of K6(B)
dom (x | B) is complex-membered Element of K6(B)
((x + x) | B) /. (- x) is complex real ext-real Element of REAL
(x + x) /. (- x) is complex real ext-real Element of REAL
(x + x) . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
(x . (- x)) + (x . (- x)) is complex real ext-real set
x /. (- x) is complex real ext-real Element of REAL
(x /. (- x)) + (x . (- x)) is complex real ext-real Element of REAL
x /. (- x) is complex real ext-real Element of REAL
(x /. (- x)) + (x /. (- x)) is complex real ext-real Element of REAL
(x | B) /. (- x) is complex real ext-real Element of REAL
((x | B) /. (- x)) + (x /. (- x)) is complex real ext-real Element of REAL
(x | B) /. (- x) is complex real ext-real Element of REAL
((x | B) /. (- x)) + ((x | B) /. (- x)) is complex real ext-real Element of REAL
(x | B) . (- x) is complex real ext-real set
((x | B) . (- x)) + ((x | B) /. (- x)) is complex real ext-real Element of REAL
(x | B) . (- x) is complex real ext-real set
((x | B) . (- x)) + ((x | B) . (- x)) is complex real ext-real set
(x | B) . x is complex real ext-real set
- ((x | B) . x) is complex real ext-real set
(- ((x | B) . x)) + ((x | B) . (- x)) is complex real ext-real set
(x | B) . x is complex real ext-real set
- ((x | B) . x) is complex real ext-real set
(- ((x | B) . x)) + (- ((x | B) . x)) is complex real ext-real set
((x | B) . x) + ((x | B) . x) is complex real ext-real set
- (((x | B) . x) + ((x | B) . x)) is complex real ext-real set
(x | B) /. x is complex real ext-real Element of REAL
((x | B) /. x) + ((x | B) . x) is complex real ext-real Element of REAL
- (((x | B) /. x) + ((x | B) . x)) is complex real ext-real Element of REAL
(x | B) /. x is complex real ext-real Element of REAL
((x | B) /. x) + ((x | B) /. x) is complex real ext-real Element of REAL
- (((x | B) /. x) + ((x | B) /. x)) is complex real ext-real Element of REAL

(x /. x) + ((x | B) /. x) is complex real ext-real Element of REAL
- ((x /. x) + ((x | B) /. x)) is complex real ext-real Element of REAL

(x /. x) + (x /. x) is complex real ext-real Element of REAL
- ((x /. x) + (x /. x)) is complex real ext-real Element of REAL

(x . x) + (x /. x) is complex real ext-real Element of REAL
- ((x . x) + (x /. x)) is complex real ext-real Element of REAL

(x . x) + (x . x) is complex real ext-real set
- ((x . x) + (x . x)) is complex real ext-real set
(x + x) . x is complex real ext-real set
- ((x + x) . x) is complex real ext-real set
(x + x) /. x is complex real ext-real Element of REAL
- ((x + x) /. x) is complex real ext-real Element of REAL
((x + x) | B) /. x is complex real ext-real Element of REAL
- (((x + x) | B) /. x) is complex real ext-real Element of REAL
B is complex-membered () Element of K6(COMPLEX)

dom ((x + x) | B) is complex-membered Element of K6(B)
K6(B) is set

((x + x) | B) . (- x) is complex real ext-real set
((x + x) | B) . x is complex real ext-real set
dom (x | B) is complex-membered Element of K6(B)
dom (x | B) is complex-membered Element of K6(B)
((x + x) | B) /. (- x) is complex real ext-real Element of REAL
(x + x) /. (- x) is complex real ext-real Element of REAL
(x + x) . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
(x . (- x)) + (x . (- x)) is complex real ext-real set
x /. (- x) is complex real ext-real Element of REAL
(x /. (- x)) + (x . (- x)) is complex real ext-real Element of REAL
x /. (- x) is complex real ext-real Element of REAL
(x /. (- x)) + (x /. (- x)) is complex real ext-real Element of REAL
(x | B) /. (- x) is complex real ext-real Element of REAL
((x | B) /. (- x)) + (x /. (- x)) is complex real ext-real Element of REAL
(x | B) /. (- x) is complex real ext-real Element of REAL
((x | B) /. (- x)) + ((x | B) /. (- x)) is complex real ext-real Element of REAL
(x | B) . (- x) is complex real ext-real set
((x | B) . (- x)) + ((x | B) /. (- x)) is complex real ext-real Element of REAL
(x | B) . (- x) is complex real ext-real set
((x | B) . (- x)) + ((x | B) . (- x)) is complex real ext-real set
(x | B) . x is complex real ext-real set
((x | B) . x) + ((x | B) . (- x)) is complex real ext-real set
(x | B) . x is complex real ext-real set
((x | B) . x) + ((x | B) . x) is complex real ext-real set
(x | B) /. x is complex real ext-real Element of REAL
((x | B) /. x) + ((x | B) . x) is complex real ext-real Element of REAL
(x | B) /. x is complex real ext-real Element of REAL
((x | B) /. x) + ((x | B) /. x) is complex real ext-real Element of REAL

(x /. x) + ((x | B) /. x) is complex real ext-real Element of REAL

(x /. x) + (x /. x) is complex real ext-real Element of REAL

(x . x) + (x /. x) is complex real ext-real Element of REAL

(x . x) + (x . x) is complex real ext-real set
(x + x) . x is complex real ext-real set
(x + x) /. x is complex real ext-real Element of REAL
((x + x) | B) /. x is complex real ext-real Element of REAL
B is complex-membered () Element of K6(COMPLEX)

dom ((x - x) | B) is complex-membered Element of K6(B)
K6(B) is set

((x - x) | B) . (- x) is complex real ext-real set
((x - x) | B) . x is complex real ext-real set
- (((x - x) | B) . x) is complex real ext-real set
dom (x | B) is complex-membered Element of K6(B)
dom (x | B) is complex-membered Element of K6(B)
((x - x) | B) /. (- x) is complex real ext-real Element of REAL
(x - x) /. (- x) is complex real ext-real Element of REAL
(x - x) . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
(x . (- x)) - (x . (- x)) is complex real ext-real set
- (x . (- x)) is complex real ext-real set
(x . (- x)) + (- (x . (- x))) is complex real ext-real set
x /. (- x) is complex real ext-real Element of REAL
(x /. (- x)) - (x . (- x)) is complex real ext-real Element of REAL
(x /. (- x)) + (- (x . (- x))) is complex real ext-real set
x /. (- x) is complex real ext-real Element of REAL
(x /. (- x)) - (x /. (- x)) is complex real ext-real Element of REAL
- (x /. (- x)) is complex real ext-real set
(x /. (- x)) + (- (x /. (- x))) is complex real ext-real set
(x | B) /. (- x) is complex real ext-real Element of REAL
((x | B) /. (- x)) - (x /. (- x)) is complex real ext-real Element of REAL
((x | B) /. (- x)) + (- (x /. (- x))) is complex real ext-real set
(x | B) /. (- x) is complex real ext-real Element of REAL
((x | B) /. (- x)) - ((x | B) /. (- x)) is complex real ext-real Element of REAL
- ((x | B) /. (- x)) is complex real ext-real set
((x | B) /. (- x)) + (- ((x | B) /. (- x))) is complex real ext-real set
(x | B) . (- x) is complex real ext-real set
((x | B) . (- x)) - ((x | B) /. (- x)) is complex real ext-real Element of REAL
((x | B) . (- x)) + (- ((x | B) /. (- x))) is complex real ext-real set
(x | B) . (- x) is complex real ext-real set
((x | B) . (- x)) - ((x | B) . (- x)) is complex real ext-real set
- ((x | B) . (- x)) is complex real ext-real set
((x | B) . (- x)) + (- ((x | B) . (- x))) is complex real ext-real set
(x | B) . x is complex real ext-real set
- ((x | B) . x) is complex real ext-real set
(- ((x | B) . x)) - ((x | B) . (- x)) is complex real ext-real set
(- ((x | B) . x)) + (- ((x | B) . (- x))) is complex real ext-real set
(x | B) . x is complex real ext-real set
- ((x | B) . x) is complex real ext-real set
(- ((x | B) . x)) - (- ((x | B) . x)) is complex real ext-real set
- (- ((x | B) . x)) is complex real ext-real set
(- ((x | B) . x)) + (- (- ((x | B) . x))) is complex real ext-real set
((x | B) . x) - ((x | B) . x) is complex real ext-real set
((x | B) . x) + (- ((x | B) . x)) is complex real ext-real set
- (((x | B) . x) - ((x | B) . x)) is complex real ext-real set
(x | B) /. x is complex real ext-real Element of REAL
((x | B) /. x) - ((x | B) . x) is complex real ext-real Element of REAL
((x | B) /. x) + (- ((x | B) . x)) is complex real ext-real set
- (((x | B) /. x) - ((x | B) . x)) is complex real ext-real Element of REAL
(x | B) /. x is complex real ext-real Element of REAL
((x | B) /. x) - ((x | B) /. x) is complex real ext-real Element of REAL
- ((x | B) /. x) is complex real ext-real set
((x | B) /. x) + (- ((x | B) /. x)) is complex real ext-real set
- (((x | B) /. x) - ((x | B) /. x)) is complex real ext-real Element of REAL

(x /. x) - ((x | B) /. x) is complex real ext-real Element of REAL
(x /. x) + (- ((x | B) /. x)) is complex real ext-real set
- ((x /. x) - ((x | B) /. x)) is complex real ext-real Element of REAL

(x /. x) - (x /. x) is complex real ext-real Element of REAL
- (x /. x) is complex real ext-real set
(x /. x) + (- (x /. x)) is complex real ext-real set
- ((x /. x) - (x /. x)) is complex real ext-real Element of REAL

(x . x) - (x /. x) is complex real ext-real Element of REAL
(x . x) + (- (x /. x)) is complex real ext-real set
- ((x . x) - (x /. x)) is complex real ext-real Element of REAL

(x . x) - (x . x) is complex real ext-real set
- (x . x) is complex real ext-real set
(x . x) + (- (x . x)) is complex real ext-real set
- ((x . x) - (x . x)) is complex real ext-real set
(x - x) . x is complex real ext-real set
- ((x - x) . x) is complex real ext-real set
(x - x) /. x is complex real ext-real Element of REAL
- ((x - x) /. x) is complex real ext-real Element of REAL
((x - x) | B) /. x is complex real ext-real Element of REAL
- (((x - x) | B) /. x) is complex real ext-real Element of REAL
B is complex-membered () Element of K6(COMPLEX)

dom ((x - x) | B) is complex-membered Element of K6(B)
K6(B) is set

((x - x) | B) . (- x) is complex real ext-real set
((x - x) | B) . x is complex real ext-real set
dom (x | B) is complex-membered Element of K6(B)
dom (x | B) is complex-membered Element of K6(B)
((x - x) | B) /. (- x) is complex real ext-real Element of REAL
(x - x) /. (- x) is complex real ext-real Element of REAL
(x - x) . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
(x . (- x)) - (x . (- x)) is complex real ext-real set
- (x . (- x)) is complex real ext-real set
(x . (- x)) + (- (x . (- x))) is complex real ext-real set
x /. (- x) is complex real ext-real Element of REAL
(x /. (- x)) - (x . (- x)) is complex real ext-real Element of REAL
(x /. (- x)) + (- (x . (- x))) is complex real ext-real set
x /. (- x) is complex real ext-real Element of REAL
(x /. (- x)) - (x /. (- x)) is complex real ext-real Element of REAL
- (x /. (- x)) is complex real ext-real set
(x /. (- x)) + (- (x /. (- x))) is complex real ext-real set
(x | B) /. (- x) is complex real ext-real Element of REAL
((x | B) /. (- x)) - (x /. (- x)) is complex real ext-real Element of REAL
((x | B) /. (- x)) + (- (x /. (- x))) is complex real ext-real set
(x | B) /. (- x) is complex real ext-real Element of REAL
((x | B) /. (- x)) - ((x | B) /. (- x)) is complex real ext-real Element of REAL
- ((x | B) /. (- x)) is complex real ext-real set
((x | B) /. (- x)) + (- ((x | B) /. (- x))) is complex real ext-real set
(x | B) . (- x) is complex real ext-real set
((x | B) . (- x)) - ((x | B) /. (- x)) is complex real ext-real Element of REAL
((x | B) . (- x)) + (- ((x | B) /. (- x))) is complex real ext-real set
(x | B) . (- x) is complex real ext-real set
((x | B) . (- x)) - ((x | B) . (- x)) is complex real ext-real set
- ((x | B) . (- x)) is complex real ext-real set
((x | B) . (- x)) + (- ((x | B) . (- x))) is complex real ext-real set
(x | B) . x is complex real ext-real set
((x | B) . x) - ((x | B) . (- x)) is complex real ext-real set
((x | B) . x) + (- ((x | B) . (- x))) is complex real ext-real set
(x | B) . x is complex real ext-real set
((x | B) . x) - ((x | B) . x) is complex real ext-real set
- ((x | B) . x) is complex real ext-real set
((x | B) . x) + (- ((x | B) . x)) is complex real ext-real set
(x | B) /. x is complex real ext-real Element of REAL
((x | B) /. x) - ((x | B) . x) is complex real ext-real Element of REAL
((x | B) /. x) + (- ((x | B) . x)) is complex real ext-real set
(x | B) /. x is complex real ext-real Element of REAL
((x | B) /. x) - ((x | B) /. x) is complex real ext-real Element of REAL
- ((x | B) /. x) is complex real ext-real set
((x | B) /. x) + (- ((x | B) /. x)) is complex real ext-real set

(x /. x) - ((x | B) /. x) is complex real ext-real Element of REAL
(x /. x) + (- ((x | B) /. x)) is complex real ext-real set

(x /. x) - (x /. x) is complex real ext-real Element of REAL
- (x /. x) is complex real ext-real set
(x /. x) + (- (x /. x)) is complex real ext-real set

(x . x) - (x /. x) is complex real ext-real Element of REAL
(x . x) + (- (x /. x)) is complex real ext-real set

(x . x) - (x . x) is complex real ext-real set
- (x . x) is complex real ext-real set
(x . x) + (- (x . x)) is complex real ext-real set
(x - x) . x is complex real ext-real set
(x - x) /. x is complex real ext-real Element of REAL
((x - x) | B) /. x is complex real ext-real Element of REAL

x is complex-membered () Element of K6(COMPLEX)

dom ((B (#) x) | x) is complex-membered Element of K6(x)
K6(x) is set

((B (#) x) | x) . (- x) is complex real ext-real set
((B (#) x) | x) . x is complex real ext-real set
- (((B (#) x) | x) . x) is complex real ext-real set
dom (x | x) is complex-membered Element of K6(x)
((B (#) x) | x) /. (- x) is complex real ext-real Element of REAL
(B (#) x) /. (- x) is complex real ext-real Element of REAL
(B (#) x) . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
B * (x . (- x)) is complex real ext-real Element of REAL
x /. (- x) is complex real ext-real Element of REAL
B * (x /. (- x)) is complex real ext-real Element of REAL
(x | x) /. (- x) is complex real ext-real Element of REAL
B * ((x | x) /. (- x)) is complex real ext-real Element of REAL
(x | x) . (- x) is complex real ext-real set
B * ((x | x) . (- x)) is complex real ext-real Element of REAL
(x | x) . x is complex real ext-real set
- ((x | x) . x) is complex real ext-real set
B * (- ((x | x) . x)) is complex real ext-real Element of REAL
B * ((x | x) . x) is complex real ext-real Element of REAL
- (B * ((x | x) . x)) is complex real ext-real Element of REAL
(x | x) /. x is complex real ext-real Element of REAL
B * ((x | x) /. x) is complex real ext-real Element of REAL
- (B * ((x | x) /. x)) is complex real ext-real Element of REAL

B * (x /. x) is complex real ext-real Element of REAL
- (B * (x /. x)) is complex real ext-real Element of REAL

B * (x . x) is complex real ext-real Element of REAL
- (B * (x . x)) is complex real ext-real Element of REAL
(B (#) x) . x is complex real ext-real set
- ((B (#) x) . x) is complex real ext-real set
(B (#) x) /. x is complex real ext-real Element of REAL
- ((B (#) x) /. x) is complex real ext-real Element of REAL
((B (#) x) | x) /. x is complex real ext-real Element of REAL
- (((B (#) x) | x) /. x) is complex real ext-real Element of REAL

x is complex-membered () Element of K6(COMPLEX)

dom ((B (#) x) | x) is complex-membered Element of K6(x)
K6(x) is set

((B (#) x) | x) . (- x) is complex real ext-real set
((B (#) x) | x) . x is complex real ext-real set
dom (x | x) is complex-membered Element of K6(x)
((B (#) x) | x) /. (- x) is complex real ext-real Element of REAL
(B (#) x) /. (- x) is complex real ext-real Element of REAL
(B (#) x) . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
B * (x . (- x)) is complex real ext-real Element of REAL
x /. (- x) is complex real ext-real Element of REAL
B * (x /. (- x)) is complex real ext-real Element of REAL
(x | x) /. (- x) is complex real ext-real Element of REAL
B * ((x | x) /. (- x)) is complex real ext-real Element of REAL
(x | x) . (- x) is complex real ext-real set
B * ((x | x) . (- x)) is complex real ext-real Element of REAL
(x | x) . x is complex real ext-real set
B * ((x | x) . x) is complex real ext-real Element of REAL
(x | x) /. x is complex real ext-real Element of REAL
B * ((x | x) /. x) is complex real ext-real Element of REAL

B * (x /. x) is complex real ext-real Element of REAL

B * (x . x) is complex real ext-real Element of REAL
(B (#) x) . x is complex real ext-real set
(B (#) x) /. x is complex real ext-real Element of REAL
((B (#) x) | x) /. x is complex real ext-real Element of REAL
B is complex-membered () Element of K6(COMPLEX)

dom ((- x) | B) is complex-membered Element of K6(B)
K6(B) is set

((- x) | B) . (- x) is complex real ext-real set
((- x) | B) . x is complex real ext-real set
- (((- x) | B) . x) is complex real ext-real set
dom (x | B) is complex-membered Element of K6(B)
((- x) | B) /. (- x) is complex real ext-real Element of REAL
(- x) /. (- x) is complex real ext-real Element of REAL
(- x) . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set