:: 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
- (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) . (- 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 set
(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)) 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 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 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))
- 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
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
- (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) . (- 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 | 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 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) | 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))
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
(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) . (- 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 set
(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)) " 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 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 set
- ((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))
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 (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
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
(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) . (- 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 | 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 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 ") | 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))
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
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
|.(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 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 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 | B) /. x) is complex real ext-real Element of REAL
|.(- ((x | B) /. 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 /. 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 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.| | 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))
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
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
|.(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 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 set
|.((x | B) . x).| is complex real ext-real set
(x | B) /. x is complex real ext-real Element of REAL
|.((x | B) /. x).| is complex real ext-real set
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 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
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 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))
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))
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) * ((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 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 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))
x - B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
- B is complex real ext-real set
(- B) + x is Relation-like Function-like set
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (x - B) is complex-membered ext-real-membered real-membered Element of K6(REAL)
(x - B) | x is Relation-like REAL -defined x -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((x - B) | 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
((x - B) | x) . (- x) is complex real ext-real set
((x - B) | x) . x is complex real ext-real set
dom (x | x) is complex-membered Element of K6(x)
((x - B) | 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) is complex real ext-real set
(x . (- x)) - B is complex real ext-real Element of REAL
(x . (- x)) + (- B) is complex real ext-real set
x /. (- x) is complex real ext-real Element of REAL
(x /. (- x)) - B is complex real ext-real Element of REAL
(x /. (- x)) + (- B) is complex real ext-real set
(x | x) /. (- x) is complex real ext-real Element of REAL
((x | x) /. (- x)) - B is complex real ext-real Element of REAL
((x | x) /. (- x)) + (- B) is complex real ext-real set
(x | x) . (- x) is complex real ext-real set
((x | x) . (- x)) - B is complex real ext-real Element of REAL
((x | x) . (- x)) + (- B) is complex real ext-real set
(x | x) . x is complex real ext-real set
((x | x) . x) - B is complex real ext-real Element of REAL
((x | x) . x) + (- B) is complex real ext-real set
(x | x) /. x is complex real ext-real Element of REAL
((x | x) /. x) - B is complex real ext-real Element of REAL
((x | x) /. x) + (- B) is complex real ext-real set
x /. x is complex real ext-real Element of REAL
(x /. x) - B is complex real ext-real Element of REAL
(x /. x) + (- B) is complex real ext-real set
x . x is complex real ext-real set
(x . x) - B is complex real ext-real Element of REAL
(x . x) + (- B) 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 - B) | 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 ^2 is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x (#) x is Relation-like Function-like 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))
x ^2 is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x (#) x is Relation-like Function-like 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))
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
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) 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) " 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-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
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-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
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)) / ((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
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) / ((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) " 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 Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
- B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(- 1) (#) B is Relation-like Function-like set
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (- B) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
(- B) . (- x) is complex real ext-real set
(- B) . x is complex real ext-real set
- ((- B) . x) is complex real ext-real set
B . (- x) is complex real ext-real set
- (B . (- x)) is complex real ext-real set
B . x is complex real ext-real set
- (B . x) is complex real ext-real set
- (- (B . x)) is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
- B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(- 1) (#) B is Relation-like Function-like set
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (- B) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
(- B) . (- x) is complex real ext-real set
(- B) . x is complex real ext-real set
B . (- x) is complex real ext-real set
- (B . (- x)) is complex real ext-real set
B . x is complex real ext-real set
- (B . x) is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
B " is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (B ") is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
(B ") . (- x) is complex real ext-real set
(B ") . x is complex real ext-real set
- ((B ") . x) is complex real ext-real set
B . (- x) is complex real ext-real set
(B . (- x)) " is complex real ext-real set
B . x is complex real ext-real set
- (B . x) is complex real ext-real set
(- (B . x)) " is complex real ext-real set
(B . x) " is complex real ext-real set
- ((B . x) ") is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
B " is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (B ") is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
(B ") . (- x) is complex real ext-real set
(B ") . x is complex real ext-real set
B . (- x) is complex real ext-real set
(B . (- x)) " is complex real ext-real set
B . x is complex real ext-real set
(B . x) " is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
|.B.| is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom |.B.| is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
|.B.| . (- x) is complex real ext-real set
|.B.| . x is complex real ext-real set
B . (- x) is complex real ext-real set
|.(B . (- x)).| is complex real ext-real set
B . x is complex real ext-real set
- (B . x) is complex real ext-real set
|.(- (B . x)).| is complex real ext-real set
|.(B . x).| is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
|.B.| is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom |.B.| is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
|.B.| . (- x) is complex real ext-real set
|.B.| . x is complex real ext-real set
B . (- x) is complex real ext-real set
|.(B . (- x)).| is complex real ext-real set
B . x is complex real ext-real set
|.(B . x).| is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
B ^2 is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
B (#) B is Relation-like Function-like set
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (B ^2) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
(B ^2) . (- x) is complex real ext-real set
(B ^2) . x is complex real ext-real set
B . (- x) is complex real ext-real set
(B . (- x)) ^2 is set
(B . (- x)) * (B . (- x)) is complex real ext-real set
B . x is complex real ext-real set
- (B . x) is complex real ext-real set
(- (B . x)) ^2 is set
(- (B . x)) * (- (B . x)) is complex real ext-real set
(B . x) ^2 is set
(B . x) * (B . x) is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
B ^2 is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
B (#) B is Relation-like Function-like set
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (B ^2) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- x is complex real ext-real Element of REAL
(B ^2) . (- x) is complex real ext-real set
(B ^2) . x is complex real ext-real set
B . (- x) is complex real ext-real set
(B . (- x)) ^2 is set
(B . (- x)) * (B . (- x)) is complex real ext-real set
B . x is complex real ext-real set
(B . x) ^2 is set
(B . x) * (B . x) is complex real ext-real set
B is complex real ext-real Element of REAL
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)
x is complex real ext-real Element of REAL
- 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
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 set
B + (x . x) is complex real ext-real Element of REAL
B is complex real ext-real Element of REAL
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 REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
- B is complex real ext-real set
(- B) + x is Relation-like Function-like set
dom x is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (x - B) is complex-membered ext-real-membered real-membered Element of K6(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 . (- x) is complex real ext-real set
(x . (- x)) - B is complex real ext-real Element of REAL
(x . (- x)) + (- B) is complex real ext-real set
x . x is complex real ext-real set
(x . x) - B is complex real ext-real Element of REAL
(x . x) + (- B) is complex real ext-real set
B is complex real ext-real Element of REAL
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)
x is complex real ext-real Element of REAL
- 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 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 set
- (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 Element of REAL
B is complex real ext-real Element of REAL
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)
x is complex real ext-real Element of REAL
- 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
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 set
B * (x . x) is complex real ext-real Element of REAL
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
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) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
B + x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (B + x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- 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 set
B . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
(B . (- x)) + (x . (- x)) is complex real ext-real set
B . x is complex real ext-real set
- (B . x) is complex real ext-real set
(- (B . 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
(- (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
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
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) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
B + x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (B + x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- 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) is complex real ext-real set
x . (- x) is complex real ext-real set
(B . (- x)) + (x . (- x)) is complex real ext-real set
B . x is complex real ext-real set
(B . x) + (x . (- x)) is complex real ext-real set
x . x is complex real ext-real set
(B . x) + (x . x) is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
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) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
B - 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
B + (- x) is Relation-like Function-like set
dom (B - x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- 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 set
B . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
(B . (- x)) - (x . (- x)) is complex real ext-real set
- (x . (- x)) is complex real ext-real set
(B . (- x)) + (- (x . (- x))) is complex real ext-real set
B . x is complex real ext-real set
- (B . 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
x . x is complex real ext-real set
- (x . x) is complex real ext-real set
(- (B . x)) - (- (x . x)) is complex real ext-real set
- (- (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
(B . x) + (- (x . x)) is complex real ext-real set
- ((B . x) - (x . x)) is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
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) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
B - 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
B + (- x) is Relation-like Function-like set
dom (B - x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- 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) is complex real ext-real set
x . (- x) is complex real ext-real set
(B . (- x)) - (x . (- x)) is complex real ext-real set
- (x . (- x)) is complex real ext-real set
(B . (- x)) + (- (x . (- x))) is complex real ext-real set
B . 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
x . x is complex real ext-real set
(B . x) - (x . x) is complex real ext-real set
- (x . x) is complex real ext-real set
(B . x) + (- (x . x)) is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
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) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
B (#) x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (B (#) x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- 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) is complex real ext-real set
x . (- x) is complex real ext-real set
(B . (- x)) * (x . (- x)) is complex real ext-real set
B . x is complex real ext-real set
- (B . x) is complex real ext-real set
(- (B . 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
(- (B . x)) * (- (x . x)) is complex real ext-real set
(B . x) * (x . x) is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
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) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
B (#) x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (B (#) x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- 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) is complex real ext-real set
x . (- x) is complex real ext-real set
(B . (- x)) * (x . (- x)) is complex real ext-real set
B . x is complex real ext-real set
(B . x) * (x . (- x)) is complex real ext-real set
x . x is complex real ext-real set
(B . x) * (x . x) is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
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) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
B (#) x is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (B (#) x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- 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 set
B . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
(B . (- x)) * (x . (- x)) is complex real ext-real set
B . x is complex real ext-real set
(B . 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
(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
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
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) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
B /" 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
B (#) (x ") is Relation-like Function-like set
dom (B /" x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- 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) is complex real ext-real set
x . (- x) is complex real ext-real set
(B . (- x)) / (x . (- x)) is complex real ext-real set
(x . (- x)) " is complex real ext-real set
(B . (- x)) * ((x . (- x)) ") is complex real ext-real set
B . x is complex real ext-real set
- (B . 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
x . x is complex real ext-real set
- (x . x) is complex real ext-real set
(- (B . x)) / (- (x . x)) is complex real ext-real set
(- (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
(x . x) " is complex real ext-real set
(B . x) * ((x . x) ") is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
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) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
B /" 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
B (#) (x ") is Relation-like Function-like set
dom (B /" x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- 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) is complex real ext-real set
x . (- x) is complex real ext-real set
(B . (- x)) / (x . (- x)) is complex real ext-real set
(x . (- x)) " is complex real ext-real set
(B . (- x)) * ((x . (- x)) ") is complex real ext-real set
B . 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
x . x is complex real ext-real set
(B . x) / (x . x) is complex real ext-real set
(x . x) " is complex real ext-real set
(B . x) * ((x . x) ") is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
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) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
B /" 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
B (#) (x ") is Relation-like Function-like set
dom (B /" x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- 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 set
B . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
(B . (- x)) / (x . (- x)) is complex real ext-real set
(x . (- x)) " is complex real ext-real set
(B . (- x)) * ((x . (- x)) ") is complex real ext-real set
B . x is complex real ext-real set
- (B . 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
x . x is complex real ext-real set
(- (B . x)) / (x . x) is complex real ext-real set
(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
(B . x) * ((x . x) ") is complex real ext-real set
- ((B . x) / (x . x)) is complex real ext-real set
B is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom B is complex-membered ext-real-membered real-membered Element of K6(REAL)
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) /\ (dom x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
B /" 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
B (#) (x ") is Relation-like Function-like set
dom (B /" x) is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex real ext-real Element of REAL
- 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 set
B . (- x) is complex real ext-real set
x . (- x) is complex real ext-real set
(B . (- x)) / (x . (- x)) is complex real ext-real set
(x . (- x)) " is complex real ext-real set
(B . (- x)) * ((x . (- x)) ") is complex real ext-real set
B . 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
x . x is complex real ext-real set
- (x . x) is complex real ext-real set
(B . x) / (- (x . x)) is complex real ext-real set
(- (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
(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
B is non zero Relation-like REAL -defined REAL -valued Function-like total V33( REAL , REAL ) V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
B . x is complex real ext-real Element of REAL
sgn x is complex real ext-real Element of REAL
B is non zero Relation-like REAL -defined REAL -valued Function-like total V33( REAL , REAL ) V36() V37() V38() Element of K6(K7(REAL,REAL))
x is non zero Relation-like REAL -defined REAL -valued Function-like total V33( REAL , REAL ) V36() V37() V38() Element of K6(K7(REAL,REAL))
x is complex real ext-real Element of REAL
B . x is complex real ext-real Element of REAL
x . x is complex real ext-real Element of REAL
sgn x is complex real ext-real Element of REAL
() is non zero Relation-like REAL -defined REAL -valued Function-like total V33( REAL , REAL ) V36() V37() V38() Element of K6(K7(REAL,REAL))
B is complex real ext-real set
() . B is complex real ext-real set
sgn B is complex real ext-real set
B is complex real ext-real set
() . B is complex real ext-real set
sgn B is complex real ext-real set
() . 0 is complex real ext-real Element of REAL
sgn 0 is complex real ext-real Element of REAL
B is complex real ext-real set
- B is complex real ext-real set
() . (- B) is complex real ext-real set
() . B is complex real ext-real set
- (() . B) is complex real ext-real set
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
dom () is non zero complex-membered ext-real-membered real-membered Element of K6(REAL)
() | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (() | B) is complex-membered ext-real-membered real-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
(() | B) . (- x) is complex real ext-real set
(() | B) . x is complex real ext-real set
- ((() | B) . x) is complex real ext-real set
(() | B) /. (- 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 is complex real ext-real Element of REAL
- (() /. x) is complex real ext-real Element of REAL
(() | B) /. x is complex real ext-real Element of REAL
- ((() | B) /. x) is complex real ext-real Element of REAL
B is complex real ext-real set
absreal . B is complex real ext-real set
abs B is complex real ext-real Element of REAL
B is complex real ext-real set
absreal . B is complex real ext-real set
- B is complex real ext-real set
abs B is complex real ext-real Element of REAL
B is complex real ext-real set
- B is complex real ext-real set
absreal . (- B) is complex real ext-real set
absreal . B is complex real ext-real set
- (- B) is complex real ext-real set
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
dom absreal is non zero complex-membered ext-real-membered real-membered Element of K6(REAL)
absreal | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (absreal | B) is complex-membered ext-real-membered real-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
(absreal | B) . (- x) is complex real ext-real set
(absreal | B) . x is complex real ext-real set
(absreal | B) /. (- x) is complex real ext-real Element of REAL
absreal /. (- x) is complex real ext-real Element of REAL
absreal . (- x) is complex real ext-real Element of REAL
absreal /. x is complex real ext-real Element of REAL
absreal . x is complex real ext-real Element of REAL
(absreal | B) /. x is complex real ext-real Element of REAL
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
sin | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (sin | B) is complex-membered ext-real-membered real-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
(sin | B) . (- x) is complex real ext-real set
(sin | B) . x is complex real ext-real set
- ((sin | B) . x) is complex real ext-real set
(sin | B) /. (- x) is complex real ext-real Element of REAL
sin /. (- x) is complex real ext-real Element of REAL
sin . (- x) is complex real ext-real Element of REAL
sin /. x is complex real ext-real Element of REAL
sin . x is complex real ext-real Element of REAL
- (sin /. x) is complex real ext-real Element of REAL
(sin | B) /. x is complex real ext-real Element of REAL
- ((sin | B) /. x) is complex real ext-real Element of REAL
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
cos | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (cos | B) is complex-membered ext-real-membered real-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
(cos | B) . (- x) is complex real ext-real set
(cos | B) . x is complex real ext-real set
(cos | B) /. (- x) is complex real ext-real Element of REAL
cos /. (- x) is complex real ext-real Element of REAL
cos . (- x) is complex real ext-real Element of REAL
cos /. x is complex real ext-real Element of REAL
cos . x is complex real ext-real Element of REAL
(cos | B) /. x is complex real ext-real Element of REAL
B is complex set
- B is complex set
B is complex real ext-real Element of REAL
- B is complex real ext-real Element of REAL
sin . (- B) is complex real ext-real Element of REAL
sin . B is complex real ext-real Element of REAL
- (sin . B) is complex real ext-real Element of REAL
B is complex real ext-real Element of REAL
- B is complex real ext-real Element of REAL
cos . (- B) is complex real ext-real Element of REAL
cos . B is complex real ext-real Element of REAL
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
dom sinh is non zero complex-membered ext-real-membered real-membered Element of K6(REAL)
sinh | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (sinh | B) is complex-membered ext-real-membered real-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
(sinh | B) . (- x) is complex real ext-real set
(sinh | B) . x is complex real ext-real set
- ((sinh | B) . x) is complex real ext-real set
(sinh | B) /. (- x) is complex real ext-real Element of REAL
sinh /. (- x) is complex real ext-real Element of REAL
sinh . (- x) is complex real ext-real Element of REAL
sinh /. x is complex real ext-real Element of REAL
sinh . x is complex real ext-real Element of REAL
- (sinh /. x) is complex real ext-real Element of REAL
(sinh | B) /. x is complex real ext-real Element of REAL
- ((sinh | B) /. x) is complex real ext-real Element of REAL
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
dom cosh is non zero complex-membered ext-real-membered real-membered Element of K6(REAL)
cosh | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (cosh | B) is complex-membered ext-real-membered real-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
(cosh | B) . (- x) is complex real ext-real set
(cosh | B) . x is complex real ext-real set
(cosh | B) /. (- x) is complex real ext-real Element of REAL
cosh /. (- x) is complex real ext-real Element of REAL
cosh . (- x) is complex real ext-real Element of REAL
cosh /. x is complex real ext-real Element of REAL
cosh . x is complex real ext-real Element of REAL
(cosh | B) /. x is complex real ext-real Element of REAL
B is complex set
- B is complex set
dom sinh is non zero complex-membered ext-real-membered real-membered Element of K6(REAL)
B is complex real ext-real Element of REAL
- B is complex real ext-real Element of REAL
sinh . (- B) is complex real ext-real Element of REAL
sinh . B is complex real ext-real Element of REAL
- (sinh . B) is complex real ext-real Element of REAL
B is complex set
- B is complex set
dom cosh is non zero complex-membered ext-real-membered real-membered Element of K6(REAL)
B is complex real ext-real Element of REAL
- B is complex real ext-real Element of REAL
cosh . (- B) is complex real ext-real Element of REAL
cosh . B is complex real ext-real Element of REAL
B is complex-membered () Element of K6(COMPLEX)
tan | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (tan | 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
tan . (- x) is complex real ext-real set
tan . x is complex real ext-real set
- (tan . x) is complex real ext-real set
tan (- x) is complex real ext-real Element of REAL
sin (- x) is set
K138(sin,(- x)) is complex real ext-real Element of REAL
cos (- x) is set
K138(cos,(- x)) is complex real ext-real Element of REAL
(sin (- x)) / (cos (- x)) is set
tan x is complex real ext-real Element of REAL
sin x is set
K138(sin,x) is complex real ext-real Element of REAL
cos x is set
K138(cos,x) is complex real ext-real Element of REAL
(sin x) / (cos x) is set
- (tan 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
(tan | B) . (- x) is complex real ext-real set
(tan | B) . x is complex real ext-real set
- ((tan | B) . x) is complex real ext-real set
(tan | B) /. (- x) is complex real ext-real Element of REAL
tan /. (- x) is complex real ext-real Element of REAL
tan . (- x) is complex real ext-real set
tan . x is complex real ext-real set
- (tan . x) is complex real ext-real set
tan /. x is complex real ext-real Element of REAL
- (tan /. x) is complex real ext-real Element of REAL
(tan | B) /. x is complex real ext-real Element of REAL
- ((tan | B) /. x) is complex real ext-real Element of REAL
B is complex-membered () Element of K6(COMPLEX)
tan | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (tan | 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
tan . (- x) is complex real ext-real set
tan . x is complex real ext-real set
- (tan . x) is complex real ext-real set
cos . x is complex real ext-real Element of REAL
tan (- x) is complex real ext-real Element of REAL
sin (- x) is set
K138(sin,(- x)) is complex real ext-real Element of REAL
cos (- x) is set
K138(cos,(- x)) is complex real ext-real Element of REAL
(sin (- x)) / (cos (- x)) is set
tan x is complex real ext-real Element of REAL
sin x is set
K138(sin,x) is complex real ext-real Element of REAL
cos x is set
K138(cos,x) is complex real ext-real Element of REAL
(sin x) / (cos x) is set
- (tan 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
(tan | B) . (- x) is complex real ext-real set
(tan | B) . x is complex real ext-real set
- ((tan | B) . x) is complex real ext-real set
(tan | B) /. (- x) is complex real ext-real Element of REAL
tan /. (- x) is complex real ext-real Element of REAL
tan . (- x) is complex real ext-real set
tan . x is complex real ext-real set
- (tan . x) is complex real ext-real set
tan /. x is complex real ext-real Element of REAL
- (tan /. x) is complex real ext-real Element of REAL
(tan | B) /. x is complex real ext-real Element of REAL
- ((tan | B) /. x) is complex real ext-real Element of REAL
B is complex-membered () Element of K6(COMPLEX)
cot | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (cot | 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
cot . (- x) is complex real ext-real set
cot . x is complex real ext-real set
- (cot . x) is complex real ext-real set
sin . x is complex real ext-real Element of REAL
cot (- x) is complex real ext-real Element of REAL
cos (- x) is set
K138(cos,(- x)) is complex real ext-real Element of REAL
sin (- x) is set
K138(sin,(- x)) is complex real ext-real Element of REAL
(cos (- x)) / (sin (- x)) is set
cot x is complex real ext-real Element of REAL
cos x is set
K138(cos,x) is complex real ext-real Element of REAL
sin x is set
K138(sin,x) is complex real ext-real Element of REAL
(cos x) / (sin x) is set
- (cot 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
(cot | B) . (- x) is complex real ext-real set
(cot | B) . x is complex real ext-real set
- ((cot | B) . x) is complex real ext-real set
(cot | B) /. (- x) is complex real ext-real Element of REAL
cot /. (- x) is complex real ext-real Element of REAL
cot . (- x) is complex real ext-real set
cot . x is complex real ext-real set
- (cot . x) is complex real ext-real set
cot /. x is complex real ext-real Element of REAL
- (cot /. x) is complex real ext-real Element of REAL
(cot | B) /. x is complex real ext-real Element of REAL
- ((cot | B) /. x) is complex real ext-real Element of REAL
B is complex-membered () Element of K6(COMPLEX)
arctan | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (arctan | 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
arctan . (- x) is complex real ext-real set
arctan . x is complex real ext-real set
- (arctan . x) is complex real ext-real set
arctan x is complex real ext-real Element of REAL
K138(arctan,x) is complex real ext-real Element of REAL
arctan (- x) is complex real ext-real Element of REAL
K138(arctan,(- x)) is complex real ext-real Element of REAL
- (arctan (- 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
(arctan | B) . (- x) is complex real ext-real set
(arctan | B) . x is complex real ext-real set
- ((arctan | B) . x) is complex real ext-real set
(arctan | B) /. (- x) is complex real ext-real Element of REAL
arctan /. (- x) is complex real ext-real Element of REAL
arctan . (- x) is complex real ext-real set
arctan . x is complex real ext-real set
- (arctan . x) is complex real ext-real set
arctan /. x is complex real ext-real Element of REAL
- (arctan /. x) is complex real ext-real Element of REAL
(arctan | B) /. x is complex real ext-real Element of REAL
- ((arctan | B) /. x) is complex real ext-real Element of REAL
|.sin.| is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
|.cos.| is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
sin " is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
cos " is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
- sin is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(- 1) (#) sin is Relation-like Function-like set
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
- cos is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(- 1) (#) cos is Relation-like Function-like set
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
sin ^2 is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
sin (#) sin is Relation-like Function-like set
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
cos ^2 is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
cos (#) cos is Relation-like Function-like set
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
sec is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
K367(REAL,REAL,cos) is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom sec is complex-membered ext-real-membered real-membered Element of K6(REAL)
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
sec | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (sec | B) is complex-membered ext-real-membered real-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
sec . (- x) is complex real ext-real set
sec . x is complex real ext-real set
cos . (- x) is complex real ext-real Element of REAL
(cos . (- x)) " is complex real ext-real Element of REAL
cos . x is complex real ext-real Element of REAL
(cos . 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
(sec | B) . (- x) is complex real ext-real set
(sec | B) . x is complex real ext-real set
(sec | B) /. (- x) is complex real ext-real Element of REAL
sec /. (- x) is complex real ext-real Element of REAL
sec . (- x) is complex real ext-real set
sec . x is complex real ext-real set
sec /. x is complex real ext-real Element of REAL
(sec | B) /. x is complex real ext-real Element of REAL
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
x is complex real ext-real set
cos . x is complex real ext-real set
cos " {0} is complex-membered ext-real-membered real-membered Element of K6(REAL)
(dom cos) \ (cos " {0}) is complex-membered ext-real-membered real-membered Element of K6(REAL)
cosec is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
K367(REAL,REAL,sin) is Relation-like REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom cosec is complex-membered ext-real-membered real-membered Element of K6(REAL)
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
cosec | B is Relation-like REAL -defined B -defined REAL -defined REAL -valued Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (cosec | B) is complex-membered ext-real-membered real-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
cosec . (- x) is complex real ext-real set
cosec . x is complex real ext-real set
- (cosec . x) is complex real ext-real set
sin . (- x) is complex real ext-real Element of REAL
(sin . (- x)) " is complex real ext-real Element of REAL
sin . x is complex real ext-real Element of REAL
- (sin . x) is complex real ext-real Element of REAL
(- (sin . x)) " is complex real ext-real Element of REAL
(sin . x) " is complex real ext-real Element of REAL
- ((sin . 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
(cosec | B) . (- x) is complex real ext-real set
(cosec | B) . x is complex real ext-real set
- ((cosec | B) . x) is complex real ext-real set
(cosec | B) /. (- x) is complex real ext-real Element of REAL
cosec /. (- x) is complex real ext-real Element of REAL
cosec . (- x) is complex real ext-real set
cosec . x is complex real ext-real set
- (cosec . x) is complex real ext-real set
cosec /. x is complex real ext-real Element of REAL
- (cosec /. x) is complex real ext-real Element of REAL
(cosec | B) /. x is complex real ext-real Element of REAL
- ((cosec | B) /. x) is complex real ext-real Element of REAL
B is complex-membered ext-real-membered real-membered () Element of K6(REAL)
x is complex real ext-real set
sin . x is complex real ext-real set
sin " {0} is complex-membered ext-real-membered real-membered Element of K6(REAL)
(dom sin) \ (sin " {0}) is complex-membered ext-real-membered real-membered Element of K6(REAL)