:: FUNCT_8 semantic presentation

REAL is non zero V48() complex-membered ext-real-membered real-membered V143() set
NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V143() Element of K6(REAL)
K6(REAL) is set
omega is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V143() set
K6(omega) is set
K6(NAT) is set
1 is non zero natural complex real ext-real positive non negative V46() V47() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
K7(1,1) is Relation-like RAT -valued INT -valued V36() V37() V38() V39() set
RAT is non zero V48() complex-membered ext-real-membered real-membered rational-membered V143() set
INT is non zero V48() complex-membered ext-real-membered real-membered rational-membered integer-membered V143() 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
2 is non zero natural complex real ext-real positive non negative V46() V47() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
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 (TOP-REAL 2) is set
0c is zero Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional V36() V37() V38() V39() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V143() set
{0c,1} is non zero set
K7(COMPLEX,COMPLEX) is Relation-like V36() 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
K7(INT,INT) is Relation-like RAT -valued INT -valued V36() V37() V38() 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
0 is zero natural complex real ext-real non positive non negative Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional V36() V37() V38() V39() V46() V47() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V143() Element of NAT
- 1 is non zero complex real ext-real non positive negative Element of REAL
absreal is non zero Relation-like REAL -defined REAL -valued Function-like total V33( REAL , REAL ) V36() V37() V38() Element of K6(K7(REAL,REAL))
- 1 is non zero complex real ext-real non positive negative set
PI is complex real ext-real Element of REAL
PI / 2 is complex real ext-real Element of REAL
2 " is non zero complex real ext-real positive non negative set
PI * (2 ") is complex real ext-real 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)
tan is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
sin is non zero Relation-like REAL -defined REAL -valued Function-like total V33( REAL , REAL ) V36() V37() V38() Element of K6(K7(REAL,REAL))
cos is non zero Relation-like REAL -defined REAL -valued Function-like total V33( REAL , REAL ) V36() V37() V38() Element of K6(K7(REAL,REAL))
K364(REAL,REAL,sin,cos) is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom tan is complex-membered ext-real-membered real-membered Element of K6(REAL)
cot is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
K364(REAL,REAL,cos,sin) is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
[.(- 1),1.] is complex-membered ext-real-membered real-membered Element of K6(REAL)
arctan is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom arctan is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom sin is non zero complex-membered ext-real-membered real-membered Element of K6(REAL)
dom cos is non zero complex-membered ext-real-membered real-membered Element of K6(REAL)
K138(cos,0) is complex real ext-real Element of REAL
K138(sin,0) is complex real ext-real Element of REAL
cosh is non zero Relation-like REAL -defined REAL -valued Function-like total V33( REAL , REAL ) V36() V37() V38() Element of K6(K7(REAL,REAL))
sinh is non zero Relation-like REAL -defined REAL -valued Function-like total V33( REAL , REAL ) V36() V37() V38() Element of K6(K7(REAL,REAL))
tanh is non zero Relation-like REAL -defined REAL -valued Function-like total V33( REAL , REAL ) V36() V37() V38() Element of K6(K7(REAL,REAL))
{0} is non zero functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
dom cot is complex-membered ext-real-membered real-membered Element of K6(REAL)
K6(COMPLEX) is set
[#] COMPLEX is complex-membered Element of K6(COMPLEX)
B is complex set
- B is complex set
[#] REAL is complex-membered ext-real-membered real-membered Element of K6(REAL)
B is complex set
- B is complex set
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
B is complex set
- B is complex set
dom 0c is zero Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional V36() V37() V38() V39() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V143() set
B is Relation-like set
B is Relation-like () set
dom B is set
B is complex-membered set
x is complex-membered set
K7(B,x) is Relation-like V36() set
K6(K7(B,x)) is set
B is complex-membered set
x is complex-membered set
K7(B,x) is Relation-like V36() set
K6(K7(B,x)) is set
B is complex-membered set
x is complex-membered 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))
x is complex-membered set
x is complex-membered set
K7(x,x) is Relation-like V36() set
K6(K7(x,x)) is set
B is complex-membered set
x is complex-membered set
K7(B,x) is Relation-like V36() set
K6(K7(B,x)) is set
B is complex-membered set
x is complex-membered set
K7(B,x) is Relation-like V36() set
K6(K7(B,x)) is set
B is complex-membered set
x is complex-membered 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))
x is complex-membered set
x is complex-membered set
K7(x,x) is Relation-like V36() set
K6(K7(x,x)) is set
B is complex-membered () Element of K6(COMPLEX)
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (x | B) is complex-membered Element of K6(B)
K6(B) is set
x is complex real ext-real Element of REAL
- 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 set
(x . x) + (x . (- x)) is complex real ext-real set
x is complex real ext-real Element of REAL
- 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
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 /. 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 | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
x . x is complex real ext-real set
- 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 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 is complex real ext-real Element of REAL
x . x is complex real ext-real set
- 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 is complex real ext-real Element of REAL
x . x is complex real ext-real set
- 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 is complex real ext-real Element of REAL
x . x is complex real ext-real set
- 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
B is complex-membered () Element of K6(COMPLEX)
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (x | B) is complex-membered Element of K6(B)
K6(B) is set
x is complex real ext-real Element of REAL
- 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) - (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 is complex real ext-real Element of REAL
- 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 . 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 is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
x . x is complex real ext-real set
- 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 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) - ((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 is complex real ext-real Element of REAL
x . x is complex real ext-real set
- 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
x is complex real ext-real Element of REAL
x . x is complex real ext-real set
- 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
x is complex real ext-real Element of REAL
x . x is complex real ext-real set
- 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
B is complex-membered () Element of K6(COMPLEX)
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
x . x is complex real ext-real set
- 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 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 /. 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 is complex real ext-real Element of REAL
x . x is complex real ext-real set
- 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
B is complex-membered () Element of K6(COMPLEX)
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (x | B) is complex-membered Element of K6(B)
K6(B) is set
x is complex real ext-real Element of REAL
- 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 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 is complex real ext-real Element of REAL
- 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
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 /. 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 is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
x . x is complex real ext-real set
- 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 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 /. 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 is complex real ext-real Element of REAL
x . x is complex real ext-real set
- 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
B is complex-membered () Element of K6(COMPLEX)
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (x | B) is complex-membered Element of K6(B)
K6(B) is set
x is complex real ext-real Element of REAL
- 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) / (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 is complex real ext-real Element of REAL
- 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 . 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
B is complex-membered () Element of K6(COMPLEX)
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
x . x is complex real ext-real set
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (x | B) is complex-membered Element of K6(B)
K6(B) is set
- x is complex real ext-real Element of REAL
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 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 is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
x . x is complex real ext-real set
abs x is complex real ext-real Element of REAL
x . (abs x) is complex real ext-real set
dom (x | B) is complex-membered Element of K6(B)
K6(B) is set
- x is complex real ext-real Element of REAL
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
x /. x is complex real ext-real Element of REAL
B is complex-membered () Element of K6(COMPLEX)
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (x | B) is complex-membered Element of K6(B)
K6(B) is set
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
- 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
abs x is complex real ext-real Element of REAL
x . (abs x) is complex real ext-real set
abs (- x) is complex real ext-real Element of REAL
- (- x) is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
- 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 . 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
B is complex-membered () Element of K6(COMPLEX)
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x + x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
(dom x) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (x + x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
(x + x) | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((x + x) | B) is complex-membered Element of K6(B)
K6(B) is set
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
((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 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 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 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 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)
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x + x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
(dom x) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (x + x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
(x + x) | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((x + x) | B) is complex-membered Element of K6(B)
K6(B) is set
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
((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 is complex real ext-real Element of REAL
(x /. x) + ((x | B) /. 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 . 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 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)
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x - x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
- x is Relation-like Function-like V36() set
(- 1) (#) x is Relation-like Function-like set
x + (- x) is Relation-like Function-like set
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
(dom x) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (x - x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
(x - x) | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((x - x) | B) is complex-membered Element of K6(B)
K6(B) is set
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
((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 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 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 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 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
- ((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)
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x - x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
- x is Relation-like Function-like V36() set
(- 1) (#) x is Relation-like Function-like set
x + (- x) is Relation-like Function-like set
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
(dom x) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (x - x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
(x - x) | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((x - x) | B) is complex-membered Element of K6(B)
K6(B) is set
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
((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 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 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 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) 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
B is complex real ext-real Element of REAL
x is complex-membered () Element of K6(COMPLEX)
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
B (#) x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (B (#) x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
(B (#) x) | x is Relation-like REAL -defined x -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((B (#) x) | x) is complex-membered Element of K6(x)
K6(x) is set
x | x is Relation-like REAL -defined x -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
((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
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
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 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
B is complex real ext-real Element of REAL
x is complex-membered () Element of K6(COMPLEX)
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
B (#) x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (B (#) x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
(B (#) x) | x is Relation-like REAL -defined x -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((B (#) x) | x) is complex-membered Element of K6(x)
K6(x) is set
x | x is Relation-like REAL -defined x -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
((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
x /. x is complex real ext-real Element of REAL
B * (x /. x) is complex real ext-real Element of REAL
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 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)
x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
- x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(- 1) (#) x is Relation-like Function-like set
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (- x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
(- x) | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((- x) | B) is complex-membered Element of K6(B)
K6(B) is set
x | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
- 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
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