:: QUATERN2 semantic presentation

REAL is set

K6(REAL) is set

QUATERNION is non zero set

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

K119(REAL,0,1,0,1) is V16() Function-like V30({0,1}, REAL ) Element of K6(K7({0,1},REAL))
{0,1} is non zero set
K7({0,1},REAL) is V16() set
K6(K7({0,1},REAL)) is set
(- ()) * <i> is quaternion set
() + ((- ()) * <i>) is quaternion set

K147(NAT,0,1,2,3,0,0,1,0) is V16() Function-like V30(K138(0,1,2,3), NAT ) Element of K6(K7(K138(0,1,2,3),NAT))
K138(0,1,2,3) is set
K7(K138(0,1,2,3),NAT) is V16() set
K6(K7(K138(0,1,2,3),NAT)) is set
K118(0,1,0,0) is set
K118(2,3,1,0) is set
K115(K118(0,1,0,0),K118(2,3,1,0)) is V16() Function-like set

(- ()) * <j> is quaternion set
(() + ((- ()) * <i>)) + ((- ()) * <j>) is quaternion Element of QUATERNION

K147(NAT,0,1,2,3,0,0,0,1) is V16() Function-like V30(K138(0,1,2,3), NAT ) Element of K6(K7(K138(0,1,2,3),NAT))
K118(2,3,0,1) is set
K115(K118(0,1,0,0),K118(2,3,0,1)) is V16() Function-like set

(- ()) * <k> is quaternion set
((() + ((- ()) * <i>)) + ((- ()) * <j>)) + ((- ()) * <k>) is quaternion Element of QUATERNION

(() ^2) + (() ^2) is complex ext-real real Element of REAL

((() ^2) + (() ^2)) + (() ^2) is complex ext-real real Element of REAL

(((() ^2) + (() ^2)) + (() ^2)) + (() ^2) is complex ext-real real Element of REAL
sqrt ((((() ^2) + (() ^2)) + (() ^2)) + (() ^2)) is complex ext-real real Element of REAL

(() ^2) + (() ^2) is complex ext-real real Element of REAL

((() ^2) + (() ^2)) + (() ^2) is complex ext-real real Element of REAL

(((() ^2) + (() ^2)) + (() ^2)) + (() ^2) is complex ext-real real Element of REAL
sqrt ((((() ^2) + (() ^2)) + (() ^2)) + (() ^2)) is complex ext-real real Element of REAL
c1 is quaternion set

c1 * c1 is complex ext-real real set

c2 * c2 is complex ext-real real set
(c1 ^2) + (c2 ^2) is complex ext-real real set

c3 * c3 is complex ext-real real set
((c1 ^2) + (c2 ^2)) + (c3 ^2) is complex ext-real real set

y1 * y1 is complex ext-real real set
(((c1 ^2) + (c2 ^2)) + (c3 ^2)) + (y1 ^2) is complex ext-real real set

c1 * c1 is complex ext-real real set

c2 * c2 is complex ext-real real set
(c1 ^2) + (c2 ^2) is complex ext-real real set

c3 * c3 is complex ext-real real set
((c1 ^2) + (c2 ^2)) + (c3 ^2) is complex ext-real real set

y1 * y1 is complex ext-real real set
(((c1 ^2) + (c2 ^2)) + (c3 ^2)) + (y1 ^2) is complex ext-real real set

[*c1,c2,c3,y1*] is quaternion Element of QUATERNION

c1 + (c2 * <i>) is quaternion set

(c1 + (c2 * <i>)) + (c3 * <j>) is quaternion Element of QUATERNION

((c1 + (c2 * <i>)) + (c3 * <j>)) + (y1 * <k>) is quaternion Element of QUATERNION
[*0,1*] is Element of COMPLEX

c2 * 1 is complex ext-real real Element of REAL
[*(c2 * 0),(c2 * 1),(c2 * 0),(c2 * 0)*] is quaternion Element of QUATERNION
[*0,c2,0,0*] is quaternion Element of QUATERNION

c3 * 1 is complex ext-real real Element of REAL
[*(c3 * 0),(c3 * 0),(c3 * 1),(c2 * 0)*] is quaternion Element of QUATERNION
[*0,0,c3,0*] is quaternion Element of QUATERNION

y1 * 1 is complex ext-real real Element of REAL
[*(y1 * 0),(y1 * 0),(y1 * 0),(y1 * 1)*] is quaternion Element of QUATERNION
[*0,0,0,y1*] is quaternion Element of QUATERNION

[*(c1 + 0),c2,0,0*] is quaternion Element of QUATERNION
[*c1,c2,0,0*] is quaternion Element of QUATERNION

[*(c1 + 0),(c2 + 0),(0 + c3),()*] is quaternion Element of QUATERNION
[*c1,c2,c3,0*] is quaternion Element of QUATERNION

[*(c1 + 0),(c2 + 0),(0 + c3),(0 + y1)*] is quaternion Element of QUATERNION
c1 is quaternion set
c2 is quaternion set
c1 + c2 is quaternion Element of QUATERNION
c3 is quaternion set
(c1 + c2) + c3 is quaternion Element of QUATERNION
c2 + c3 is quaternion Element of QUATERNION
c1 + (c2 + c3) is quaternion Element of QUATERNION

[*y1,w1,z1,x2*] is quaternion Element of QUATERNION

[*y2,w2,z2,c1*] is quaternion Element of QUATERNION

[*c2,q0,q1,q2*] is quaternion Element of QUATERNION
y2 + c2 is complex ext-real real Element of REAL
w2 + q0 is complex ext-real real Element of REAL
z2 + q1 is complex ext-real real Element of REAL
c1 + q2 is complex ext-real real Element of REAL
[*(y2 + c2),(w2 + q0),(z2 + q1),(c1 + q2)*] is quaternion Element of QUATERNION
y1 + y2 is complex ext-real real Element of REAL
w1 + w2 is complex ext-real real Element of REAL
z1 + z2 is complex ext-real real Element of REAL
x2 + c1 is complex ext-real real Element of REAL
[*(y1 + y2),(w1 + w2),(z1 + z2),(x2 + c1)*] is quaternion Element of QUATERNION
[*(y1 + y2),(w1 + w2),(z1 + z2),(x2 + c1)*] + [*c2,q0,q1,q2*] is quaternion Element of QUATERNION
(y1 + y2) + c2 is complex ext-real real Element of REAL
(w1 + w2) + q0 is complex ext-real real Element of REAL
(z1 + z2) + q1 is complex ext-real real Element of REAL
(x2 + c1) + q2 is complex ext-real real Element of REAL
[*((y1 + y2) + c2),((w1 + w2) + q0),((z1 + z2) + q1),((x2 + c1) + q2)*] is quaternion Element of QUATERNION
y1 + (y2 + c2) is complex ext-real real Element of REAL
w1 + (w2 + q0) is complex ext-real real Element of REAL
z1 + (z2 + q1) is complex ext-real real Element of REAL
x2 + (c1 + q2) is complex ext-real real Element of REAL
[*(y1 + (y2 + c2)),(w1 + (w2 + q0)),(z1 + (z2 + q1)),(x2 + (c1 + q2))*] is quaternion Element of QUATERNION
() is quaternion Element of QUATERNION
c1 is quaternion set
c1 + () is quaternion Element of QUATERNION
is Element of COMPLEX

[*c2,c3,y1,w1*] is quaternion Element of QUATERNION

[*(c2 + 0),(c3 + 0),(y1 + 0),(w1 + 0)*] is quaternion Element of QUATERNION

[*c1,c2,c3,y1*] is quaternion Element of QUATERNION
- [*c1,c2,c3,y1*] is quaternion Element of QUATERNION

[*(- c1),(- c2),(- c3),(- y1)*] is quaternion Element of QUATERNION
[*c1,c2,c3,y1*] + [*(- c1),(- c2),(- c3),(- y1)*] is quaternion Element of QUATERNION
c1 - c1 is complex ext-real real Element of REAL

c1 + (- c1) is complex ext-real real set
c2 - c2 is complex ext-real real Element of REAL

c2 + (- c2) is complex ext-real real set
c3 - c3 is complex ext-real real Element of REAL

c3 + (- c3) is complex ext-real real set
y1 - y1 is complex ext-real real Element of REAL

y1 + (- y1) is complex ext-real real set
[*(c1 - c1),(c2 - c2),(c3 - c3),(y1 - y1)*] is quaternion Element of QUATERNION
is Element of COMPLEX

[*c1,c2,c3,y1*] is quaternion Element of QUATERNION

c1 - w1 is complex ext-real real Element of REAL

c1 + (- w1) is complex ext-real real set

c2 - z1 is complex ext-real real Element of REAL

c2 + (- z1) is complex ext-real real set

c3 - x2 is complex ext-real real Element of REAL

c3 + (- x2) is complex ext-real real set

[*w1,z1,x2,y2*] is quaternion Element of QUATERNION
[*c1,c2,c3,y1*] - [*w1,z1,x2,y2*] is quaternion Element of QUATERNION
- [*w1,z1,x2,y2*] is quaternion set
[*c1,c2,c3,y1*] + (- [*w1,z1,x2,y2*]) is quaternion set
y1 - y2 is complex ext-real real Element of REAL

y1 + (- y2) is complex ext-real real set
[*(c1 - w1),(c2 - z1),(c3 - x2),(y1 - y2)*] is quaternion Element of QUATERNION

[*(- w1),(- z1),(- x2),(- y2)*] is quaternion Element of QUATERNION
[*c1,c2,c3,y1*] + [*(- w1),(- z1),(- x2),(- y2)*] is quaternion Element of QUATERNION
c1 is quaternion set
c2 is quaternion set
c1 - c2 is quaternion Element of QUATERNION
- c2 is quaternion set
c1 + (- c2) is quaternion set
c3 is quaternion set
(c1 - c2) + c3 is quaternion Element of QUATERNION
c1 + c3 is quaternion Element of QUATERNION
(c1 + c3) - c2 is quaternion Element of QUATERNION
(c1 + c3) + (- c2) is quaternion set
c1 is quaternion set
c2 is quaternion set
c1 + c2 is quaternion Element of QUATERNION
(c1 + c2) - c2 is quaternion Element of QUATERNION
- c2 is quaternion set
(c1 + c2) + (- c2) is quaternion set
c2 - c2 is quaternion Element of QUATERNION
c2 + (- c2) is quaternion set
c1 + (c2 - c2) is quaternion Element of QUATERNION
c1 + () is quaternion Element of QUATERNION
c1 is quaternion set
c2 is quaternion set
c1 - c2 is quaternion Element of QUATERNION
- c2 is quaternion set
c1 + (- c2) is quaternion set
(c1 - c2) + c2 is quaternion Element of QUATERNION
c1 + c2 is quaternion Element of QUATERNION
(c1 + c2) - c2 is quaternion Element of QUATERNION
(c1 + c2) + (- c2) is quaternion set
c1 is quaternion set

(- c2) * c1 is quaternion set
c2 * c1 is quaternion set
- (c2 * c1) is quaternion Element of QUATERNION

[*c3,y1,w1,z1*] is quaternion Element of QUATERNION
(- c2) * c3 is complex ext-real real Element of REAL
(- c2) * y1 is complex ext-real real Element of REAL
(- c2) * w1 is complex ext-real real Element of REAL
(- c2) * z1 is complex ext-real real Element of REAL
[*((- c2) * c3),((- c2) * y1),((- c2) * w1),((- c2) * z1)*] is quaternion Element of QUATERNION
c2 * c3 is complex ext-real real Element of REAL
- (c2 * c3) is complex ext-real real Element of REAL
c2 * y1 is complex ext-real real Element of REAL
- (c2 * y1) is complex ext-real real Element of REAL
c2 * w1 is complex ext-real real Element of REAL
- (c2 * w1) is complex ext-real real Element of REAL
c2 * z1 is complex ext-real real Element of REAL
- (c2 * z1) is complex ext-real real Element of REAL
[*(- (c2 * c3)),(- (c2 * y1)),(- (c2 * w1)),(- (c2 * z1))*] is quaternion Element of QUATERNION
[*(c2 * c3),(c2 * y1),(c2 * w1),(c2 * z1)*] is quaternion Element of QUATERNION
- [*(c2 * c3),(c2 * y1),(c2 * w1),(c2 * z1)*] is quaternion Element of QUATERNION
[*(c2 * c3),(c2 * y1),(c2 * w1),(c2 * z1)*] + [*(- (c2 * c3)),(- (c2 * y1)),(- (c2 * w1)),(- (c2 * z1))*] is quaternion Element of QUATERNION
(c2 * c3) + (- (c2 * c3)) is complex ext-real real Element of REAL
(c2 * y1) + (- (c2 * y1)) is complex ext-real real Element of REAL
(c2 * w1) + (- (c2 * w1)) is complex ext-real real Element of REAL
(c2 * z1) + (- (c2 * z1)) is complex ext-real real Element of REAL
[*((c2 * c3) + (- (c2 * c3))),((c2 * y1) + (- (c2 * y1))),((c2 * w1) + (- (c2 * w1))),((c2 * z1) + (- (c2 * z1)))*] is quaternion Element of QUATERNION
is Element of COMPLEX
c1 is quaternion set

(Rea c1) ^2 is complex ext-real real Element of REAL
(Rea c1) * (Rea c1) is complex ext-real real set

(Im1 c1) ^2 is complex ext-real real Element of REAL
(Im1 c1) * (Im1 c1) is complex ext-real real set
((Rea c1) ^2) + ((Im1 c1) ^2) is complex ext-real real Element of REAL

(Im2 c1) ^2 is complex ext-real real Element of REAL
(Im2 c1) * (Im2 c1) is complex ext-real real set
(((Rea c1) ^2) + ((Im1 c1) ^2)) + ((Im2 c1) ^2) is complex ext-real real Element of REAL

(Im3 c1) ^2 is complex ext-real real Element of REAL
(Im3 c1) * (Im3 c1) is complex ext-real real set
((((Rea c1) ^2) + ((Im1 c1) ^2)) + ((Im2 c1) ^2)) + ((Im3 c1) ^2) is complex ext-real real Element of REAL
sqrt (((((Rea c1) ^2) + ((Im1 c1) ^2)) + ((Im2 c1) ^2)) + ((Im3 c1) ^2)) is complex ext-real real Element of REAL
c1 is quaternion set
(c1) is complex ext-real real Element of REAL

(Rea c1) ^2 is complex ext-real real Element of REAL
(Rea c1) * (Rea c1) is complex ext-real real set

(Im1 c1) ^2 is complex ext-real real Element of REAL
(Im1 c1) * (Im1 c1) is complex ext-real real set
((Rea c1) ^2) + ((Im1 c1) ^2) is complex ext-real real Element of REAL

(Im2 c1) ^2 is complex ext-real real Element of REAL
(Im2 c1) * (Im2 c1) is complex ext-real real set
(((Rea c1) ^2) + ((Im1 c1) ^2)) + ((Im2 c1) ^2) is complex ext-real real Element of REAL

(Im3 c1) ^2 is complex ext-real real Element of REAL
(Im3 c1) * (Im3 c1) is complex ext-real real set
((((Rea c1) ^2) + ((Im1 c1) ^2)) + ((Im2 c1) ^2)) + ((Im3 c1) ^2) is complex ext-real real Element of REAL
sqrt (((((Rea c1) ^2) + ((Im1 c1) ^2)) + ((Im2 c1) ^2)) + ((Im3 c1) ^2)) is complex ext-real real Element of REAL
c1 is quaternion set
(c1) is complex ext-real real Element of REAL

(Rea c1) ^2 is complex ext-real real Element of REAL
(Rea c1) * (Rea c1) is complex ext-real real set

(Im1 c1) ^2 is complex ext-real real Element of REAL
(Im1 c1) * (Im1 c1) is complex ext-real real set
((Rea c1) ^2) + ((Im1 c1) ^2) is complex ext-real real Element of REAL

(Im2 c1) ^2 is complex ext-real real Element of REAL
(Im2 c1) * (Im2 c1) is complex ext-real real set
(((Rea c1) ^2) + ((Im1 c1) ^2)) + ((Im2 c1) ^2) is complex ext-real real Element of REAL

(Im3 c1) ^2 is complex ext-real real Element of REAL
(Im3 c1) * (Im3 c1) is complex ext-real real set
((((Rea c1) ^2) + ((Im1 c1) ^2)) + ((Im2 c1) ^2)) + ((Im3 c1) ^2) is complex ext-real real Element of REAL
sqrt (((((Rea c1) ^2) + ((Im1 c1) ^2)) + ((Im2 c1) ^2)) + ((Im3 c1) ^2)) is complex ext-real real Element of REAL

is Element of COMPLEX
c1 is quaternion set
() * c1 is quaternion Element of QUATERNION

[*c2,c3,y1,w1*] is quaternion Element of QUATERNION

[*z1,x2,y2,w2*] is quaternion Element of QUATERNION
c2 * z1 is complex ext-real real Element of REAL
c3 * x2 is complex ext-real real Element of REAL
(c2 * z1) - (c3 * x2) is complex ext-real real Element of REAL
- (c3 * x2) is complex ext-real real set
(c2 * z1) + (- (c3 * x2)) is complex ext-real real set
y1 * y2 is complex ext-real real Element of REAL
((c2 * z1) - (c3 * x2)) - (y1 * y2) is complex ext-real real Element of REAL
- (y1 * y2) is complex ext-real real set
((c2 * z1) - (c3 * x2)) + (- (y1 * y2)) is complex ext-real real set
w1 * w2 is complex ext-real real Element of REAL
(((c2 * z1) - (c3 * x2)) - (y1 * y2)) - (w1 * w2) is complex ext-real real Element of REAL
- (w1 * w2) is complex ext-real real set
(((c2 * z1) - (c3 * x2)) - (y1 * y2)) + (- (w1 * w2)) is complex ext-real real set
c2 * x2 is complex ext-real real Element of REAL
c3 * z1 is complex ext-real real Element of REAL
(c2 * x2) + (c3 * z1) is complex ext-real real Element of REAL
y1 * w2 is complex ext-real real Element of REAL
((c2 * x2) + (c3 * z1)) + (y1 * w2) is complex ext-real real Element of REAL
w1 * y2 is complex ext-real real Element of REAL
(((c2 * x2) + (c3 * z1)) + (y1 * w2)) - (w1 * y2) is complex ext-real real Element of REAL
- (w1 * y2) is complex ext-real real set
(((c2 * x2) + (c3 * z1)) + (y1 * w2)) + (- (w1 * y2)) is complex ext-real real set
c2 * y2 is complex ext-real real Element of REAL
z1 * y1 is complex ext-real real Element of REAL
(c2 * y2) + (z1 * y1) is complex ext-real real Element of REAL
x2 * w1 is complex ext-real real Element of REAL
((c2 * y2) + (z1 * y1)) + (x2 * w1) is complex ext-real real Element of REAL
w2 * c3 is complex ext-real real Element of REAL
(((c2 * y2) + (z1 * y1)) + (x2 * w1)) - (w2 * c3) is complex ext-real real Element of REAL
- (w2 * c3) is complex ext-real real set
(((c2 * y2) + (z1 * y1)) + (x2 * w1)) + (- (w2 * c3)) is complex ext-real real set
c2 * w2 is complex ext-real real Element of REAL
w1 * z1 is complex ext-real real Element of REAL
(c2 * w2) + (w1 * z1) is complex ext-real real Element of REAL
c3 * y2 is complex ext-real real Element of REAL
((c2 * w2) + (w1 * z1)) + (c3 * y2) is complex ext-real real Element of REAL
y1 * x2 is complex ext-real real Element of REAL
(((c2 * w2) + (w1 * z1)) + (c3 * y2)) - (y1 * x2) is complex ext-real real Element of REAL
- (y1 * x2) is complex ext-real real set
(((c2 * w2) + (w1 * z1)) + (c3 * y2)) + (- (y1 * x2)) is complex ext-real real set
[*((((c2 * z1) - (c3 * x2)) - (y1 * y2)) - (w1 * w2)),((((c2 * x2) + (c3 * z1)) + (y1 * w2)) - (w1 * y2)),((((c2 * y2) + (z1 * y1)) + (x2 * w1)) - (w2 * c3)),((((c2 * w2) + (w1 * z1)) + (c3 * y2)) - (y1 * x2))*] is quaternion Element of QUATERNION
c1 is quaternion set
c1 * () is quaternion Element of QUATERNION

[*c2,c3,y1,w1*] is quaternion Element of QUATERNION

[*z1,x2,y2,w2*] is quaternion Element of QUATERNION
c2 * z1 is complex ext-real real Element of REAL
c3 * x2 is complex ext-real real Element of REAL
(c2 * z1) - (c3 * x2) is complex ext-real real Element of REAL
- (c3 * x2) is complex ext-real real set
(c2 * z1) + (- (c3 * x2)) is complex ext-real real set
y1 * y2 is complex ext-real real Element of REAL
((c2 * z1) - (c3 * x2)) - (y1 * y2) is complex ext-real real Element of REAL
- (y1 * y2) is complex ext-real real set
((c2 * z1) - (c3 * x2)) + (- (y1 * y2)) is complex ext-real real set
w1 * w2 is complex ext-real real Element of REAL
(((c2 * z1) - (c3 * x2)) - (y1 * y2)) - (w1 * w2) is complex ext-real real Element of REAL
- (w1 * w2) is complex ext-real real set
(((c2 * z1) - (c3 * x2)) - (y1 * y2)) + (- (w1 * w2)) is complex ext-real real set
c2 * x2 is complex ext-real real Element of REAL
c3 * z1 is complex ext-real real Element of REAL
(c2 * x2) + (c3 * z1) is complex ext-real real Element of REAL
y1 * w2 is complex ext-real real Element of REAL
((c2 * x2) + (c3 * z1)) + (y1 * w2) is complex ext-real real Element of REAL
w1 * y2 is complex ext-real real Element of REAL
(((c2 * x2) + (c3 * z1)) + (y1 * w2)) - (w1 * y2) is complex ext-real real Element of REAL
- (w1 * y2) is complex ext-real real set
(((c2 * x2) + (c3 * z1)) + (y1 * w2)) + (- (w1 * y2)) is complex ext-real real set
c2 * y2 is complex ext-real real Element of REAL
z1 * y1 is complex ext-real real Element of REAL
(c2 * y2) + (z1 * y1) is complex ext-real real Element of REAL
x2 * w1 is complex ext-real real Element of REAL
((c2 * y2) + (z1 * y1)) + (x2 * w1) is complex ext-real real Element of REAL
w2 * c3 is complex ext-real real Element of REAL
(((c2 * y2) + (z1 * y1)) + (x2 * w1)) - (w2 * c3) is complex ext-real real Element of REAL
- (w2 * c3) is complex ext-real real set
(((c2 * y2) + (z1 * y1)) + (x2 * w1)) + (- (w2 * c3)) is complex ext-real real set
c2 * w2 is complex ext-real real Element of REAL
w1 * z1 is complex ext-real real Element of REAL
(c2 * w2) + (w1 * z1) is complex ext-real real Element of REAL
c3 * y2 is complex ext-real real Element of REAL
((c2 * w2) + (w1 * z1)) + (c3 * y2) is complex ext-real real Element of REAL
y1 * x2 is complex ext-real real Element of REAL
(((c2 * w2) + (w1 * z1)) + (c3 * y2)) - (y1 * x2) is complex ext-real real Element of REAL
- (y1 * x2) is complex ext-real real set
(((c2 * w2) + (w1 * z1)) + (c3 * y2)) + (- (y1 * x2)) is complex ext-real real set
[*((((c2 * z1) - (c3 * x2)) - (y1 * y2)) - (w1 * w2)),((((c2 * x2) + (c3 * z1)) + (y1 * w2)) - (w1 * y2)),((((c2 * y2) + (z1 * y1)) + (x2 * w1)) - (w2 * c3)),((((c2 * w2) + (w1 * z1)) + (c3 * y2)) - (y1 * x2))*] is quaternion Element of QUATERNION
() is quaternion Element of QUATERNION
c1 is quaternion set
c1 * () is quaternion Element of QUATERNION
[*1,0*] is Element of COMPLEX

[*c2,c3,y1,w1*] is quaternion Element of QUATERNION
c2 * 1 is complex ext-real real Element of REAL

(c2 * 1) - (c3 * 0) is complex ext-real real Element of REAL
- (c3 * 0) is complex ext-real real set
(c2 * 1) + (- (c3 * 0)) is complex ext-real real set

((c2 * 1) - (c3 * 0)) - (y1 * 0) is complex ext-real real Element of REAL
- (y1 * 0) is complex ext-real real set
((c2 * 1) - (c3 * 0)) + (- (y1 * 0)) is complex ext-real real set

(((c2 * 1) - (c3 * 0)) - (y1 * 0)) - (w1 * 0) is complex ext-real real Element of REAL
- (w1 * 0) is complex ext-real real set
(((c2 * 1) - (c3 * 0)) - (y1 * 0)) + (- (w1 * 0)) is complex ext-real real set

c3 * 1 is complex ext-real real Element of REAL
(c2 * 0) + (c3 * 1) is complex ext-real real Element of REAL
((c2 * 0) + (c3 * 1)) + (y1 * 0) is complex ext-real real Element of REAL
(((c2 * 0) + (c3 * 1)) + (y1 * 0)) - (w1 * 0) is complex ext-real real Element of REAL
(((c2 * 0) + (c3 * 1)) + (y1 * 0)) + (- (w1 * 0)) is complex ext-real real set

(c2 * 0) + (1 * y1) is complex ext-real real Element of REAL

((c2 * 0) + (1 * y1)) + (0 * w1) is complex ext-real real Element of REAL

(((c2 * 0) + (1 * y1)) + (0 * w1)) - (0 * c3) is complex ext-real real Element of REAL
- (0 * c3) is complex ext-real real set
(((c2 * 0) + (1 * y1)) + (0 * w1)) + (- (0 * c3)) is complex ext-real real set
w1 * 1 is complex ext-real real Element of REAL
(c2 * 0) + (w1 * 1) is complex ext-real real Element of REAL
((c2 * 0) + (w1 * 1)) + (c3 * 0) is complex ext-real real Element of REAL
(((c2 * 0) + (w1 * 1)) + (c3 * 0)) - (y1 * 0) is complex ext-real real Element of REAL
(((c2 * 0) + (w1 * 1)) + (c3 * 0)) + (- (y1 * 0)) is complex ext-real real set
[*((((c2 * 1) - (c3 * 0)) - (y1 * 0)) - (w1 * 0)),((((c2 * 0) + (c3 * 1)) + (y1 * 0)) - (w1 * 0)),((((c2 * 0) + (1 * y1)) + (0 * w1)) - (0 * c3)),((((c2 * 0) + (w1 * 1)) + (c3 * 0)) - (y1 * 0))*] is quaternion Element of QUATERNION
c1 is quaternion set
() * c1 is quaternion Element of QUATERNION
[*1,0*] is Element of COMPLEX

[*c2,c3,y1,w1*] is quaternion Element of QUATERNION
c2 * 1 is complex ext-real real Element of REAL

(c2 * 1) - (c3 * 0) is complex ext-real real Element of REAL
- (c3 * 0) is complex ext-real real set
(c2 * 1) + (- (c3 * 0)) is complex ext-real real set

((c2 * 1) - (c3 * 0)) - (y1 * 0) is complex ext-real real Element of REAL
- (y1 * 0) is complex ext-real real set
((c2 * 1) - (c3 * 0)) + (- (y1 * 0)) is complex ext-real real set

(((c2 * 1) - (c3 * 0)) - (y1 * 0)) - (w1 * 0) is complex ext-real real Element of REAL
- (w1 * 0) is complex ext-real real set
(((c2 * 1) - (c3 * 0)) - (y1 * 0)) + (- (w1 * 0)) is complex ext-real real set

c3 * 1 is complex ext-real real Element of REAL
(c2 * 0) + (c3 * 1) is complex ext-real real Element of REAL
((c2 * 0) + (c3 * 1)) + (y1 * 0) is complex ext-real real Element of REAL
(((c2 * 0) + (c3 * 1)) + (y1 * 0)) - (w1 * 0) is complex ext-real real Element of REAL
(((c2 * 0) + (c3 * 1)) + (y1 * 0)) + (- (w1 * 0)) is complex ext-real real set

(c2 * 0) + (1 * y1) is complex ext-real real Element of REAL

((c2 * 0) + (1 * y1)) + (0 * w1) is complex ext-real real Element of REAL

(((c2 * 0) + (1 * y1)) + (0 * w1)) - (0 * c3) is complex ext-real real Element of REAL
- (0 * c3) is complex ext-real real set
(((c2 * 0) + (1 * y1)) + (0 * w1)) + (- (0 * c3)) is complex ext-real real set
w1 * 1 is complex ext-real real Element of REAL
(c2 * 0) + (w1 * 1) is complex ext-real real Element of REAL
((c2 * 0) + (w1 * 1)) + (c3 * 0) is complex ext-real real Element of REAL
(((c2 * 0) + (w1 * 1)) + (c3 * 0)) - (y1 * 0) is complex ext-real real Element of REAL
(((c2 * 0) + (w1 * 1)) + (c3 * 0)) + (- (y1 * 0)) is complex ext-real real set
[*((((c2 * 1) - (c3 * 0)) - (y1 * 0)) - (w1 * 0)),((((c2 * 0) + (c3 * 1)) + (y1 * 0)) - (w1 * 0)),((((c2 * 0) + (1 * y1)) + (0 * w1)) - (0 * c3)),((((c2 * 0) + (w1 * 1)) + (c3 * 0)) - (y1 * 0))*] is quaternion Element of QUATERNION
c1 is quaternion set
c2 is quaternion set
c1 * c2 is quaternion Element of QUATERNION
c3 is quaternion set
(c1 * c2) * c3 is quaternion Element of QUATERNION
c2 * c3 is quaternion Element of QUATERNION
c1 * (c2 * c3) is quaternion Element of QUATERNION

[*y1,w1,z1,x2*] is quaternion Element of QUATERNION

[*y2,w2,z2,c1*] is quaternion Element of QUATERNION

[*c2,q0,q1,q2*] is quaternion Element of QUATERNION
y1 * y2 is complex ext-real real Element of REAL
w1 * w2 is complex ext-real real Element of REAL
(y1 * y2) - (w1 * w2) is complex ext-real real Element of REAL
- (w1 * w2) is complex ext-real real set
(y1 * y2) + (- (w1 * w2)) is complex ext-real real set
z1 * z2 is complex ext-real real Element of REAL
((y1 * y2) - (w1 * w2)) - (z1 * z2) is complex ext-real real Element of REAL
- (z1 * z2) is complex ext-real real set
((y1 * y2) - (w1 * w2)) + (- (z1 * z2)) is complex ext-real real set
x2 * c1 is complex ext-real real Element of REAL
(((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1) is complex ext-real real Element of REAL
- (x2 * c1) is complex ext-real real set
(((y1 * y2) - (w1 * w2)) - (z1 * z2)) + (- (x2 * c1)) is complex ext-real real set
y1 * w2 is complex ext-real real Element of REAL
w1 * y2 is complex ext-real real Element of REAL
(y1 * w2) + (w1 * y2) is complex ext-real real Element of REAL
z1 * c1 is complex ext-real real Element of REAL
((y1 * w2) + (w1 * y2)) + (z1 * c1) is complex ext-real real Element of REAL
x2 * z2 is complex ext-real real Element of REAL
(((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2) is complex ext-real real Element of REAL
- (x2 * z2) is complex ext-real real set
(((y1 * w2) + (w1 * y2)) + (z1 * c1)) + (- (x2 * z2)) is complex ext-real real set
y1 * z2 is complex ext-real real Element of REAL
y2 * z1 is complex ext-real real Element of REAL
(y1 * z2) + (y2 * z1) is complex ext-real real Element of REAL
w2 * x2 is complex ext-real real Element of REAL
((y1 * z2) + (y2 * z1)) + (w2 * x2) is complex ext-real real Element of REAL
c1 * w1 is complex ext-real real Element of REAL
(((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1) is complex ext-real real Element of REAL
- (c1 * w1) is complex ext-real real set
(((y1 * z2) + (y2 * z1)) + (w2 * x2)) + (- (c1 * w1)) is complex ext-real real set
y1 * c1 is complex ext-real real Element of REAL
x2 * y2 is complex ext-real real Element of REAL
(y1 * c1) + (x2 * y2) is complex ext-real real Element of REAL
w1 * z2 is complex ext-real real Element of REAL
((y1 * c1) + (x2 * y2)) + (w1 * z2) is complex ext-real real Element of REAL
z1 * w2 is complex ext-real real Element of REAL
(((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2) is complex ext-real real Element of REAL
- (z1 * w2) is complex ext-real real set
(((y1 * c1) + (x2 * y2)) + (w1 * z2)) + (- (z1 * w2)) is complex ext-real real set
[*((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)),((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)),((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)),((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2))*] is quaternion Element of QUATERNION
[*((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)),((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)),((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)),((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2))*] * c3 is quaternion Element of QUATERNION
((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * c2 is complex ext-real real Element of REAL
((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * q0 is complex ext-real real Element of REAL
(((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * c2) - (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * q0) is complex ext-real real Element of REAL
- (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * q0) is complex ext-real real set
(((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * c2) + (- (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * q0)) is complex ext-real real set
((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q1 is complex ext-real real Element of REAL
((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * c2) - (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * q0)) - (((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q1) is complex ext-real real Element of REAL
- (((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q1) is complex ext-real real set
((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * c2) - (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * q0)) + (- (((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q1)) is complex ext-real real set
((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * q2 is complex ext-real real Element of REAL
(((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * c2) - (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * q0)) - (((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q1)) - (((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * q2) is complex ext-real real Element of REAL
- (((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * q2) is complex ext-real real set
(((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * c2) - (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * q0)) - (((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q1)) + (- (((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * q2)) is complex ext-real real set
((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q0 is complex ext-real real Element of REAL
((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * c2 is complex ext-real real Element of REAL
(((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q0) + (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * c2) is complex ext-real real Element of REAL
((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q2 is complex ext-real real Element of REAL
((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q0) + (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * c2)) + (((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q2) is complex ext-real real Element of REAL
((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * q1 is complex ext-real real Element of REAL
(((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q0) + (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * c2)) + (((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q2)) - (((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * q1) is complex ext-real real Element of REAL
- (((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * q1) is complex ext-real real set
(((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q0) + (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * c2)) + (((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q2)) + (- (((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * q1)) is complex ext-real real set
((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q1 is complex ext-real real Element of REAL
c2 * ((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) is complex ext-real real Element of REAL
(((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q1) + (c2 * ((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1))) is complex ext-real real Element of REAL
q0 * ((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) is complex ext-real real Element of REAL
((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q1) + (c2 * ((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)))) + (q0 * ((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2))) is complex ext-real real Element of REAL
q2 * ((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) is complex ext-real real Element of REAL
(((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q1) + (c2 * ((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)))) + (q0 * ((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)))) - (q2 * ((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2))) is complex ext-real real Element of REAL
- (q2 * ((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2))) is complex ext-real real set
(((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q1) + (c2 * ((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)))) + (q0 * ((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)))) + (- (q2 * ((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)))) is complex ext-real real set
((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q2 is complex ext-real real Element of REAL
((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * c2 is complex ext-real real Element of REAL
(((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q2) + (((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * c2) is complex ext-real real Element of REAL
((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * q1 is complex ext-real real Element of REAL
((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q2) + (((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * c2)) + (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * q1) is complex ext-real real Element of REAL
((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q0 is complex ext-real real Element of REAL
(((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q2) + (((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * c2)) + (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * q1)) - (((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q0) is complex ext-real real Element of REAL
- (((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q0) is complex ext-real real set
(((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q2) + (((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * c2)) + (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * q1)) + (- (((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q0)) is complex ext-real real set
[*((((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * c2) - (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * q0)) - (((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q1)) - (((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * q2)),((((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q0) + (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * c2)) + (((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q2)) - (((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * q1)),((((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q1) + (c2 * ((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)))) + (q0 * ((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)))) - (q2 * ((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)))),((((((((y1 * y2) - (w1 * w2)) - (z1 * z2)) - (x2 * c1)) * q2) + (((((y1 * c1) + (x2 * y2)) + (w1 * z2)) - (z1 * w2)) * c2)) + (((((y1 * w2) + (w1 * y2)) + (z1 * c1)) - (x2 * z2)) * q1)) - (((((y1 * z2) + (y2 * z1)) + (w2 * x2)) - (c1 * w1)) * q0))*] is quaternion Element of QUATERNION
(y1 * y2) * c2 is complex ext-real real Element of REAL
(w1 * w2) * c2 is complex ext-real real Element of REAL
((y1 * y2) * c2) - ((w1 * w2) * c2) is complex ext-real real Element of REAL
- ((w1 * w2) * c2) is complex ext-real real set
((y1 * y2) * c2) + (- ((w1 * w2) * c2)) is complex ext-real real set
(z1 * z2) * c2 is complex ext-real real Element of REAL
(((y1 * y2) * c2) - ((w1 * w2) * c2)) - ((z1 * z2) * c2) is complex ext-real real Element of REAL
- ((z1 * z2) * c2) is complex ext-real real set
(((y1 * y2) * c2) - ((w1 * w2) * c2)) + (- ((z1 * z2) * c2)) is complex ext-real real set
(x2 * c1) * c2 is complex ext-real real Element of REAL
((((y1 * y2) * c2) - ((w1 * w2) * c2)) - ((z1 * z2) * c2)) - ((x2 * c1) * c2) is complex ext-real real Element of REAL
- ((x2 * c1) * c2) is complex ext-real real set
((((y1 * y2) * c2) - ((w1 * w2) * c2)) - ((z1 * z2) * c2)) + (- ((x2 * c1) * c2)) is complex ext-real real set
(y1 * w2) * q0 is complex ext-real real Element of REAL
(w1 * y2) * q0 is complex ext-real real Element of REAL
((y1 * w2) * q0) + ((w1 * y2) * q0) is complex ext-real real Element of REAL
(z1 * c1) * q0 is complex ext-real real Element of REAL
(((y1 * w2) * q0) + ((w1 * y2) * q0)) + ((z1 * c1) * q0) is complex ext-real real Element of REAL
(x2 * z2) * q0 is complex ext-real real Element of REAL
((((y1 * w2) * q0) + ((w1 * y2) * q0)) + ((z1 * c1) * q0)) - ((x2 * z2) * q0) is complex ext-real real Element of REAL
- ((x2 * z2) * q0) is complex ext-real real set
((((y1 * w2) * q0) + ((w1 * y2) * q0)) + ((z1 * c1) * q0)) + (- ((x2 * z2) * q0)) is complex ext-real real set
(((((y1 * y2) * c2) - ((w1 * w2) * c2)) - ((z1 * z2) * c2)) - ((x2 * c1) * c2)) - (((((y1 * w2) * q0) + ((w1 * y2) * q0)) + ((z1 * c1) * q0)) - ((x2 * z2) * q0)) is complex ext-real real Element of REAL
- (((((y1 * w2) * q0) + ((w1 * y2) * q0)) + ((z1 * c1) * q0)) - ((x2 * z2) * q0)) is complex ext-real real set
(((((y1 * y2) * c2) - ((w1 * w2) * c2)) - ((z1 * z2) * c2)) - ((x2 * c1) * c2)) + (- (((((y1 * w2) * q0) + ((w1 * y2) * q0)) + ((z1 * c1) * q0)) - ((x2 * z2) * q0))) is complex ext-real real set
(y1 * z2) * q1 is complex ext-real real Element of REAL
(y2 * z1) * q1 is complex ext-real real Element of REAL
((y1 * z2) * q1) + ((y2 * z1) * q1) is complex ext-real real Element of REAL
(w2 * x2) * q1 is complex ext-real real Element of REAL
(((y1 * z2) * q1) + ((y2 * z1) * q1)) + ((w2 * x2) * q1) is complex ext-real real Element of REAL
(c1 * w1) * q1 is complex ext-real real Element of REAL
((((y1 * z2) * q1) + ((y2 * z1) * q1)) + ((w2 * x2) * q1)) - ((c1 * w1) * q1) is complex ext-real real Element of REAL
- ((c1 * w1) * q1) is complex ext-real real set
((((y1 * z2) * q1) + ((y2 * z1) * q1)) + ((w2 * x2) * q1)) + (- ((c1 * w1) * q1)) is complex ext-real real set
((((((y1 * y2) * c2) - ((w1 * w2) * c2)) - ((z1 * z2) * c2)) - ((x2 * c1) * c2)) - (((((y1 * w2) * q0) + ((w1 * y2) * q0)) + ((z1 * c1) * q0)) - ((x2 * z2) * q0))) - (((((y1 * z2) * q1) + ((y2 * z1) * q1)) + ((w2 * x2) * q1)) - ((c1 * w1) * q1)) is complex ext-real real Element of REAL
- (((((y1 * z2) * q1) + ((y2 * z1) * q1)) + ((w2 * x2) * q1)) - ((c1 * w1) * q1)) is complex ext-real real set
((((((y1 * y2) * c2) - ((w1 * w2) * c2)) - ((z1 * z2) * c2)) - ((x2 * c1) * c2)) - (((((y1 * w2) * q0) + ((w1 * y2) * q0)) + ((z1 * c1) * q0)) - ((x2 * z2) * q0))) + (- (((((y1 * z2) * q1) + ((y2 * z1) * q1)) + ((w2 * x2) * q1)) - ((c1 * w1) * q1))) is complex ext-real real set
(y1 * c1) * q2 is complex ext-real real Element of REAL
(x2 * y2) * q2 is complex ext-real real Element of REAL
((y1 * c1) * q2) + ((x2 * y2) * q2) is complex ext-real real Element of REAL
(w1 * z2) * q2 is complex ext-real real Element of REAL
(((y1 * c1) * q2) + ((x2 * y2) * q2)) + ((w1 * z2) * q2) is complex ext-real real Element of REAL
(z1 * w2) * q2 is complex ext-real real Element of REAL
((((y1 * c1) * q2) + ((x2 * y2) * q2)) + ((w1 * z2) * q2)) - ((z1 * w2) * q2) is complex ext-real real Element of REAL
- ((z1 * w2) * q2) is complex ext-real real set
((((y1 * c1) * q2) + ((x2 * y2) * q2)) + ((w1 * z2) * q2)) + (- ((z1 * w2) * q2)) is complex ext-real real set
(((((((y1 * y2) * c2) - ((w1 * w2) * c2)) - ((z1 * z2) * c2)) - ((x2 * c1) * c2)) - (((((y1 * w2) * q0) + ((w1 * y2) * q0)) + ((z1 * c1) * q0)) - ((x2 * z2) * q0))) - (((((y1 * z2) * q1) + ((y2 * z1) * q1)) + ((w2 * x2) * q1)) - ((c1 * w1) * q1))) - (((((y1 * c1) * q2) + ((x2 * y2) * q2)) + ((w1 * z2) * q2)) - ((z1 * w2) * q2)) is complex ext-real real Element of REAL
- (((((y1 * c1) * q2) + ((x2 * y2) * q2)) + ((w1 * z2) * q2)) - ((z1 * w2) * q2)) is complex ext-real real set
(((((((y1 * y2) * c2) - ((w1 * w2) * c2)) - ((z1 * z2) * c2)) - ((x2 * c1) * c2)) - (((((y1 * w2) * q0) + ((w1 * y2) * q0)) + ((z1