:: QUATERN2 semantic presentation

begin

definition
:: original: 0q
redefine func 0q -> ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;
end;

definition
:: original: 1q
redefine func 1q -> ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;
end;

theorem :: QUATERN2:1
for x, y, z, w being ( ( ) ( complex ext-real real ) Real) holds [*x : ( ( ) ( complex ext-real real ) Real) ,y : ( ( ) ( complex ext-real real ) Real) ,z : ( ( ) ( complex ext-real real ) Real) ,w : ( ( ) ( complex ext-real real ) Real) *] : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = ((x : ( ( ) ( complex ext-real real ) Real) + (y : ( ( ) ( complex ext-real real ) Real) * <i> : ( ( ) ( quaternion ) set ) ) : ( ( ) ( quaternion ) set ) ) : ( ( ) ( quaternion ) set ) + (z : ( ( ) ( complex ext-real real ) Real) * <j> : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) + (w : ( ( ) ( complex ext-real real ) Real) * <k> : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) set ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:2
for c1, c2, c3 being ( ( quaternion ) ( quaternion ) number ) holds (c1 : ( ( quaternion ) ( quaternion ) number ) + c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) + c3 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = c1 : ( ( quaternion ) ( quaternion ) number ) + (c2 : ( ( quaternion ) ( quaternion ) number ) + c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:3
for c being ( ( quaternion ) ( quaternion ) number ) holds c : ( ( quaternion ) ( quaternion ) number ) + 0q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = c : ( ( quaternion ) ( quaternion ) number ) ;

theorem :: QUATERN2:4
for x1, x2, x3, x4 being ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) holds - [*x1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,x2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,x3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,x4 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) *] : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = [*(- x1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(- x2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(- x3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(- x4 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) *] : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:5
for x1, x2, x3, x4, y1, y2, y3, y4 being ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) holds [*x1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,x2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,x3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,x4 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) *] : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) - [*y1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,y2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,y3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,y4 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) *] : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = [*(x1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - y1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(x2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - y2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(x3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - y3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(x4 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - y4 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) *] : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:6
for c1, c2, c3 being ( ( quaternion ) ( quaternion ) number ) holds (c1 : ( ( quaternion ) ( quaternion ) number ) - c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) + c3 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = (c1 : ( ( quaternion ) ( quaternion ) number ) + c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) - c2 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:7
for c1, c2 being ( ( quaternion ) ( quaternion ) number ) holds c1 : ( ( quaternion ) ( quaternion ) number ) = (c1 : ( ( quaternion ) ( quaternion ) number ) + c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) - c2 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:8
for c1, c2 being ( ( quaternion ) ( quaternion ) number ) holds c1 : ( ( quaternion ) ( quaternion ) number ) = (c1 : ( ( quaternion ) ( quaternion ) number ) - c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) + c2 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:9
for c being ( ( quaternion ) ( quaternion ) number )
for x1 being ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) holds (- x1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * c : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) set ) = - (x1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * c : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) set ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

definition
let q be ( ( quaternion ) ( quaternion ) number ) ;
:: original: |.
redefine func |.q.| -> ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ;
end;

definition
:: original: <i>
redefine func <i> -> ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;
end;

theorem :: QUATERN2:10
for r being ( ( quaternion ) ( quaternion ) number ) st r : ( ( quaternion ) ( quaternion ) number ) <> 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) > 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: QUATERN2:11
0q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = [*0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) *] : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:12
for r being ( ( quaternion ) ( quaternion ) number ) holds 0q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) * r : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: QUATERN2:13
for r being ( ( quaternion ) ( quaternion ) number ) holds r : ( ( quaternion ) ( quaternion ) number ) * 0q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: QUATERN2:14
for c being ( ( quaternion ) ( quaternion ) number ) holds c : ( ( quaternion ) ( quaternion ) number ) * 1q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = c : ( ( quaternion ) ( quaternion ) number ) ;

theorem :: QUATERN2:15
for c being ( ( quaternion ) ( quaternion ) number ) holds 1q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) * c : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = c : ( ( quaternion ) ( quaternion ) number ) ;

theorem :: QUATERN2:16
for c1, c2, c3 being ( ( quaternion ) ( quaternion ) number ) holds (c1 : ( ( quaternion ) ( quaternion ) number ) * c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) * c3 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = c1 : ( ( quaternion ) ( quaternion ) number ) * (c2 : ( ( quaternion ) ( quaternion ) number ) * c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:17
for c1, c2, c3 being ( ( quaternion ) ( quaternion ) number ) holds c1 : ( ( quaternion ) ( quaternion ) number ) * (c2 : ( ( quaternion ) ( quaternion ) number ) + c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = (c1 : ( ( quaternion ) ( quaternion ) number ) * c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) + (c1 : ( ( quaternion ) ( quaternion ) number ) * c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:18
for c1, c2, c3 being ( ( quaternion ) ( quaternion ) number ) holds (c1 : ( ( quaternion ) ( quaternion ) number ) + c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) * c3 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = (c1 : ( ( quaternion ) ( quaternion ) number ) * c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) + (c2 : ( ( quaternion ) ( quaternion ) number ) * c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:19
for c being ( ( quaternion ) ( quaternion ) number ) holds - c : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = (- 1q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) * c : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:20
for c1, c2 being ( ( quaternion ) ( quaternion ) number ) holds (- c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) * c2 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = - (c1 : ( ( quaternion ) ( quaternion ) number ) * c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:21
for c1, c2 being ( ( quaternion ) ( quaternion ) number ) holds c1 : ( ( quaternion ) ( quaternion ) number ) * (- c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = - (c1 : ( ( quaternion ) ( quaternion ) number ) * c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:22
for c1, c2 being ( ( quaternion ) ( quaternion ) number ) holds (- c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) * (- c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = c1 : ( ( quaternion ) ( quaternion ) number ) * c2 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:23
for c1, c2, c3 being ( ( quaternion ) ( quaternion ) number ) holds (c1 : ( ( quaternion ) ( quaternion ) number ) - c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) * c3 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = (c1 : ( ( quaternion ) ( quaternion ) number ) * c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) - (c2 : ( ( quaternion ) ( quaternion ) number ) * c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:24
for c1, c2, c3 being ( ( quaternion ) ( quaternion ) number ) holds c1 : ( ( quaternion ) ( quaternion ) number ) * (c2 : ( ( quaternion ) ( quaternion ) number ) - c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = (c1 : ( ( quaternion ) ( quaternion ) number ) * c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) - (c1 : ( ( quaternion ) ( quaternion ) number ) * c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:25
for x1, x2, x3, x4 being ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) holds [*x1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,x2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,x3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,x4 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) *] : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) *' : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = [*x1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(- x2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(- x3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(- x4 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) *] : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:26
for c being ( ( quaternion ) ( quaternion ) number ) holds (c : ( ( quaternion ) ( quaternion ) number ) *') : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) *' : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = c : ( ( quaternion ) ( quaternion ) number ) ;

definition
let q, r be ( ( quaternion ) ( quaternion ) number ) ;
func q / r -> ( ( ) ( ) set ) means :: QUATERN2:def 1
 ex q0, q1, q2, q3, r0, r1, r2, r3 being ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) st
( q : ( ( ) ( ) 1-sorted ) = [*q0 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,q1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,q2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,q3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) *] : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) & r : ( ( ) ( ) VectSpStr over q : ( ( ) ( ) 1-sorted ) ) = [*r0 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,r1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,r2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,r3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) *] : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) & it : ( ( Function-like V30(K7(r : ( ( ) ( ) VectSpStr over q : ( ( ) ( ) 1-sorted ) ) ,r : ( ( ) ( ) VectSpStr over q : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( V16() ) set ) ,r : ( ( ) ( ) VectSpStr over q : ( ( ) ( ) 1-sorted ) ) ) ) ( V16() Function-like V30(K7(r : ( ( ) ( ) VectSpStr over q : ( ( ) ( ) 1-sorted ) ) ,r : ( ( ) ( ) VectSpStr over q : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( V16() ) set ) ,r : ( ( ) ( ) VectSpStr over q : ( ( ) ( ) 1-sorted ) ) ) ) Element of K6(K7(K7(r : ( ( ) ( ) VectSpStr over q : ( ( ) ( ) 1-sorted ) ) ,r : ( ( ) ( ) VectSpStr over q : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( V16() ) set ) ,r : ( ( ) ( ) VectSpStr over q : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) = [*(((((r0 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q0 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + (r1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + (r2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + (r3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( ) ( ) VectSpStr over q : ( ( ) ( ) 1-sorted ) ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(((((r0 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - (r1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q0 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - (r2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + (r3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( ) ( ) VectSpStr over q : ( ( ) ( ) 1-sorted ) ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(((((r0 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + (r1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - (r2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q0 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - (r3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( ) ( ) VectSpStr over q : ( ( ) ( ) 1-sorted ) ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(((((r0 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - (r1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + (r2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q1 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - (r3 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * q0 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( ) ( ) VectSpStr over q : ( ( ) ( ) 1-sorted ) ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) *] : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) );
end;

registration
let q, r be ( ( quaternion ) ( quaternion ) number ) ;
cluster q : ( ( quaternion ) ( quaternion ) set ) / r : ( ( quaternion ) ( quaternion ) set ) : ( ( ) ( ) set ) -> quaternion ;
end;

definition
let q, r be ( ( quaternion ) ( quaternion ) number ) ;
:: original: /
redefine func q / r -> ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;
end;

theorem :: QUATERN2:27
for q, r being ( ( quaternion ) ( quaternion ) number ) holds q : ( ( quaternion ) ( quaternion ) number ) / r : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = ((((((((Rea r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Rea q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im1 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im1 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im2 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im2 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im3 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im3 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + (((((((Rea r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im1 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im1 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Rea q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im2 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im3 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im3 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im2 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * <i> : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) set ) ) : ( ( ) ( quaternion ) set ) + (((((((Rea r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im2 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im1 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im3 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im2 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Rea q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im3 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im1 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * <j> : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) + (((((((Rea r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im3 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im1 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im2 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im2 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im1 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im3 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Rea q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * <k> : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) set ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

definition
let c be ( ( quaternion ) ( quaternion ) number ) ;
func c " -> ( ( quaternion ) ( quaternion ) number ) equals :: QUATERN2:def 2
1q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) / c : ( ( ) ( ) set ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;
end;

definition
let r be ( ( quaternion ) ( quaternion ) number ) ;
:: original: "
redefine func r " -> ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;
end;

theorem :: QUATERN2:28
for r being ( ( quaternion ) ( quaternion ) number ) holds r : ( ( quaternion ) ( quaternion ) number ) " : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = ((((Rea r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - (((Im1 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * <i> : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) set ) ) : ( ( ) ( quaternion ) set ) - (((Im2 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * <j> : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) - (((Im3 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * <k> : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) set ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:29
for r being ( ( quaternion ) ( quaternion ) number ) holds
( Rea (r : ( ( quaternion ) ( quaternion ) number ) ") : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = (Rea r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) & Im1 (r : ( ( quaternion ) ( quaternion ) number ) ") : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = - ((Im1 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) & Im2 (r : ( ( quaternion ) ( quaternion ) number ) ") : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = - ((Im2 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) & Im3 (r : ( ( quaternion ) ( quaternion ) number ) ") : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = - ((Im3 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) ;

theorem :: QUATERN2:30
for q, r being ( ( quaternion ) ( quaternion ) number ) holds
( Rea (q : ( ( quaternion ) ( quaternion ) number ) / r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = (((((Rea r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Rea q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im1 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im1 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im2 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im2 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im3 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im3 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) & Im1 (q : ( ( quaternion ) ( quaternion ) number ) / r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = (((((Rea r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im1 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im1 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Rea q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im2 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im3 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im3 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im2 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) & Im2 (q : ( ( quaternion ) ( quaternion ) number ) / r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = (((((Rea r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im2 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im1 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im3 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im2 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Rea q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im3 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im1 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) & Im3 (q : ( ( quaternion ) ( quaternion ) number ) / r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = (((((Rea r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im3 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im1 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im2 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im2 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im1 q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im3 r : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Rea q : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) / (|.r : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) ;

theorem :: QUATERN2:31
for r being ( ( quaternion ) ( quaternion ) number ) st r : ( ( quaternion ) ( quaternion ) number ) <> 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
r : ( ( quaternion ) ( quaternion ) number ) * (r : ( ( quaternion ) ( quaternion ) number ) ") : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: QUATERN2:32
for r being ( ( quaternion ) ( quaternion ) number ) st r : ( ( quaternion ) ( quaternion ) number ) <> 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
(r : ( ( quaternion ) ( quaternion ) number ) ") : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) * r : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: QUATERN2:33
for c being ( ( quaternion ) ( quaternion ) number ) st c : ( ( quaternion ) ( quaternion ) number ) <> 0q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) holds
c : ( ( quaternion ) ( quaternion ) number ) / c : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = 1q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:34
for c being ( ( quaternion ) ( quaternion ) number ) holds (- c : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) " : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = - (c : ( ( quaternion ) ( quaternion ) number ) ") : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

definition
func compquaternion -> ( ( Function-like V30( QUATERNION : ( ( ) ( non zero ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) ( V16() Function-like V30( QUATERNION : ( ( ) ( non zero ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) UnOp of QUATERNION : ( ( ) ( non zero ) set ) ) means :: QUATERN2:def 3
 for c being ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) holds it : ( ( ) ( ) set ) . c : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( ) set ) = - c : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;
func addquaternion -> ( ( Function-like V30(K7(QUATERNION : ( ( ) ( non zero ) set ) ,QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( V16() ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) ( V16() Function-like V30(K7(QUATERNION : ( ( ) ( non zero ) set ) ,QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( V16() ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) BinOp of QUATERNION : ( ( ) ( non zero ) set ) ) means :: QUATERN2:def 4
 for c1, c2 being ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) holds it : ( ( ) ( ) set ) . (c1 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ,c2 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = c1 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) + c2 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;
func diffquaternion -> ( ( Function-like V30(K7(QUATERNION : ( ( ) ( non zero ) set ) ,QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( V16() ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) ( V16() Function-like V30(K7(QUATERNION : ( ( ) ( non zero ) set ) ,QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( V16() ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) BinOp of QUATERNION : ( ( ) ( non zero ) set ) ) means :: QUATERN2:def 5
 for c1, c2 being ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) holds it : ( ( ) ( ) set ) . (c1 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ,c2 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = c1 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) - c2 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;
func multquaternion -> ( ( Function-like V30(K7(QUATERNION : ( ( ) ( non zero ) set ) ,QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( V16() ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) ( V16() Function-like V30(K7(QUATERNION : ( ( ) ( non zero ) set ) ,QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( V16() ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) BinOp of QUATERNION : ( ( ) ( non zero ) set ) ) means :: QUATERN2:def 6
 for c1, c2 being ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) holds it : ( ( ) ( ) set ) . (c1 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ,c2 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = c1 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) * c2 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;
func divquaternion -> ( ( Function-like V30(K7(QUATERNION : ( ( ) ( non zero ) set ) ,QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( V16() ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) ( V16() Function-like V30(K7(QUATERNION : ( ( ) ( non zero ) set ) ,QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( V16() ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) BinOp of QUATERNION : ( ( ) ( non zero ) set ) ) means :: QUATERN2:def 7
 for c1, c2 being ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) holds it : ( ( ) ( ) set ) . (c1 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ,c2 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = c1 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) / c2 : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;
func invquaternion -> ( ( Function-like V30( QUATERNION : ( ( ) ( non zero ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) ( V16() Function-like V30( QUATERNION : ( ( ) ( non zero ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) UnOp of QUATERNION : ( ( ) ( non zero ) set ) ) means :: QUATERN2:def 8
 for c being ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) holds it : ( ( ) ( ) set ) . c : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( ) set ) = c : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) " : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;
end;

definition
func G_Quaternion -> ( ( strict ) ( strict ) addLoopStr ) means :: QUATERN2:def 9
( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = QUATERNION : ( ( ) ( non zero ) set ) & the addF of it : ( ( ) ( ) set ) : ( ( Function-like V30(K7( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V16() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( V16() Function-like V30(K7( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V16() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K6(K7(K7( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V16() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) = addquaternion : ( ( Function-like V30(K7(QUATERNION : ( ( ) ( non zero ) set ) ,QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( V16() ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) ( V16() Function-like V30(K7(QUATERNION : ( ( ) ( non zero ) set ) ,QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( V16() ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) BinOp of QUATERNION : ( ( ) ( non zero ) set ) ) & 0. it : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = 0q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) );
end;

registration
cluster G_Quaternion : ( ( strict ) ( strict ) addLoopStr ) -> non empty strict ;
end;

registration
cluster -> quaternion for ( ( ) ( ) Element of the carrier of G_Quaternion : ( ( strict ) ( non empty strict ) addLoopStr ) : ( ( ) ( non zero ) set ) ) ;
end;

registration
let x, y be ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) ;
let a, b be ( ( quaternion ) ( quaternion ) number ) ;
identify ;
end;

theorem :: QUATERN2:35
0. G_Quaternion : ( ( strict ) ( non empty strict ) addLoopStr ) : ( ( ) ( quaternion zero ) Element of the carrier of G_Quaternion : ( ( strict ) ( non empty strict ) addLoopStr ) : ( ( ) ( non zero ) set ) ) = 0q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

registration
cluster G_Quaternion : ( ( strict ) ( non empty strict ) addLoopStr ) -> strict right_complementable Abelian add-associative right_zeroed ;
end;

registration
let x be ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) ;
let a be ( ( quaternion ) ( quaternion ) number ) ;
identify ;
end;

registration
let x, y be ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) ;
let a, b be ( ( quaternion ) ( quaternion ) number ) ;
identify ;
end;

theorem :: QUATERN2:36
for x, y, z being ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) holds
( x : ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) + y : ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of the carrier of G_Quaternion : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non zero ) set ) ) = y : ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) + x : ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of the carrier of G_Quaternion : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non zero ) set ) ) & (x : ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) + y : ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) Element of the carrier of G_Quaternion : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non zero ) set ) ) + z : ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of the carrier of G_Quaternion : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non zero ) set ) ) = x : ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) + (y : ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) + z : ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) Element of the carrier of G_Quaternion : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of the carrier of G_Quaternion : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non zero ) set ) ) & x : ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) + (0. G_Quaternion : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) ) : ( ( ) ( quaternion zero ) Element of the carrier of G_Quaternion : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of the carrier of G_Quaternion : ( ( strict ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non zero ) set ) ) = x : ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) ) ;

definition
func R_Quaternion -> ( ( strict ) ( strict ) doubleLoopStr ) means :: QUATERN2:def 10
( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = QUATERNION : ( ( ) ( non zero ) set ) & the addF of it : ( ( ) ( ) set ) : ( ( Function-like V30(K7( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V16() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( V16() Function-like V30(K7( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V16() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K6(K7(K7( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V16() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) = addquaternion : ( ( Function-like V30(K7(QUATERNION : ( ( ) ( non zero ) set ) ,QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( V16() ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) ( V16() Function-like V30(K7(QUATERNION : ( ( ) ( non zero ) set ) ,QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( V16() ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) BinOp of QUATERNION : ( ( ) ( non zero ) set ) ) & the multF of it : ( ( ) ( ) set ) : ( ( Function-like V30(K7( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V16() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( V16() Function-like V30(K7( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V16() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K6(K7(K7( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V16() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) = multquaternion : ( ( Function-like V30(K7(QUATERNION : ( ( ) ( non zero ) set ) ,QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( V16() ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) ( V16() Function-like V30(K7(QUATERNION : ( ( ) ( non zero ) set ) ,QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( V16() ) set ) , QUATERNION : ( ( ) ( non zero ) set ) ) ) BinOp of QUATERNION : ( ( ) ( non zero ) set ) ) & 1. it : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = 1q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) & 0. it : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = 0q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) );
end;

registration
cluster R_Quaternion : ( ( strict ) ( strict ) doubleLoopStr ) -> non empty strict ;
end;

registration
cluster -> quaternion for ( ( ) ( ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non zero ) set ) ) ;
end;

registration
let a, b be ( ( quaternion ) ( quaternion ) number ) ;
let x, y be ( ( ) ( quaternion ) Element of ( ( ) ( non zero ) set ) ) ;
identify ;
identify ;
end;

registration
cluster R_Quaternion : ( ( strict ) ( non empty strict ) doubleLoopStr ) -> strict well-unital ;
end;

theorem :: QUATERN2:37
1. R_Quaternion : ( ( strict ) ( non empty strict unital right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( quaternion ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty strict unital right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non zero ) set ) ) = 1q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:38
1_ R_Quaternion : ( ( strict ) ( non empty strict unital right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( quaternion ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty strict unital right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non zero ) set ) ) = 1q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:39
0. R_Quaternion : ( ( strict ) ( non empty strict unital right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( quaternion zero ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty strict unital right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non zero ) set ) ) = 0q : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

registration
cluster R_Quaternion : ( ( strict ) ( non empty strict unital right_unital well-unital left_unital ) doubleLoopStr ) -> non degenerated right_complementable almost_right_invertible strict Abelian add-associative right_zeroed associative right_unital distributive left_unital ;
end;

registration
let x be ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) ;
let a be ( ( quaternion ) ( quaternion ) number ) ;
identify ;
end;

registration
let x, y be ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) ;
let a, b be ( ( quaternion ) ( quaternion ) number ) ;
identify ;
end;

definition
let z be ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) ;
:: original: *'
redefine func z *' -> ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) ;
end;

theorem :: QUATERN2:40
for z being ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) holds - z : ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) : ( ( ) ( quaternion ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) = (- (1_ R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( quaternion ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) ) : ( ( ) ( quaternion ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) * z : ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) : ( ( ) ( quaternion ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) ;

theorem :: QUATERN2:41
(0. R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( quaternion zero ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) *' : ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) = 0. R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( quaternion zero ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) ;

theorem :: QUATERN2:42
for z being ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) st z : ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) *' : ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) = 0. R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( quaternion zero ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) holds
z : ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) = 0. R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( quaternion zero ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) ;

theorem :: QUATERN2:43
(1. R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( quaternion non zero ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) *' : ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) = 1. R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( quaternion non zero ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) ;

theorem :: QUATERN2:44
|.(0. R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( quaternion zero ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: QUATERN2:45
for z being ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) st |.z : ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
z : ( ( ) ( quaternion ) Element of ( ( ) ( non zero V2() ) set ) ) = 0. R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( quaternion zero ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) ;

theorem :: QUATERN2:46
|.(1. R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( quaternion non zero ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: QUATERN2:47
(1. R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( quaternion non zero ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) " : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = 1. R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( quaternion non zero ) Element of the carrier of R_Quaternion : ( ( strict ) ( non empty non degenerated V53() right_complementable almost_right_invertible strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non zero V2() ) set ) ) ;

definition
let x, y be ( ( quaternion ) ( quaternion ) number ) ;
func x .|. y -> ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) equals :: QUATERN2:def 11
x : ( ( ) ( ) set ) * (y : ( ( ) ( ) set ) *') : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;
end;

theorem :: QUATERN2:48
for c1, c2 being ( ( quaternion ) ( quaternion ) number ) holds c1 : ( ( quaternion ) ( quaternion ) number ) .|. c2 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = [*(((((Rea c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Rea c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im1 c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im1 c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im2 c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im2 c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im3 c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im3 c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(((((Rea c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (- (Im1 c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im1 c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Rea c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im2 c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im3 c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im3 c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im2 c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(((((Rea c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (- (Im2 c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Rea c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im2 c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im1 c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im3 c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im3 c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im1 c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ,(((((Rea c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (- (Im3 c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im3 c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Rea c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) - ((Im1 c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im2 c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) + ((Im2 c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * (Im1 c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) *] : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:49
for c being ( ( quaternion ) ( quaternion ) number ) holds c : ( ( quaternion ) ( quaternion ) number ) .|. c : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = |.c : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ;

theorem :: QUATERN2:50
for c being ( ( quaternion ) ( quaternion ) number ) holds
( Rea (c : ( ( quaternion ) ( quaternion ) number ) .|. c : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = |.c : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ^2 : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) & Im1 (c : ( ( quaternion ) ( quaternion ) number ) .|. c : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & Im2 (c : ( ( quaternion ) ( quaternion ) number ) .|. c : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & Im2 (c : ( ( quaternion ) ( quaternion ) number ) .|. c : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: QUATERN2:51
for c1, c2 being ( ( quaternion ) ( quaternion ) number ) holds |.(c1 : ( ( quaternion ) ( quaternion ) number ) .|. c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) = |.c1 : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) * |.c2 : ( ( quaternion ) ( quaternion ) number ) .| : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( complex ext-real real ) Element of REAL : ( ( ) ( ) set ) ) ;

theorem :: QUATERN2:52
for c being ( ( quaternion ) ( quaternion ) number ) st c : ( ( quaternion ) ( quaternion ) number ) .|. c : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
c : ( ( quaternion ) ( quaternion ) number ) = 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real V16() non-empty empty-yielding ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: QUATERN2:53
for c1, c2, c3 being ( ( quaternion ) ( quaternion ) number ) holds (c1 : ( ( quaternion ) ( quaternion ) number ) + c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) .|. c3 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = (c1 : ( ( quaternion ) ( quaternion ) number ) .|. c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) + (c2 : ( ( quaternion ) ( quaternion ) number ) .|. c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:54
for c1, c2, c3 being ( ( quaternion ) ( quaternion ) number ) holds c1 : ( ( quaternion ) ( quaternion ) number ) .|. (c2 : ( ( quaternion ) ( quaternion ) number ) + c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = (c1 : ( ( quaternion ) ( quaternion ) number ) .|. c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) + (c1 : ( ( quaternion ) ( quaternion ) number ) .|. c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:55
for c1, c2 being ( ( quaternion ) ( quaternion ) number ) holds (- c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) .|. c2 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = - (c1 : ( ( quaternion ) ( quaternion ) number ) .|. c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:56
for c1, c2 being ( ( quaternion ) ( quaternion ) number ) holds - (c1 : ( ( quaternion ) ( quaternion ) number ) .|. c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = c1 : ( ( quaternion ) ( quaternion ) number ) .|. (- c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:57
for c1, c2 being ( ( quaternion ) ( quaternion ) number ) holds (- c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) .|. (- c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = c1 : ( ( quaternion ) ( quaternion ) number ) .|. c2 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:58
for c1, c2, c3 being ( ( quaternion ) ( quaternion ) number ) holds (c1 : ( ( quaternion ) ( quaternion ) number ) - c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) .|. c3 : ( ( quaternion ) ( quaternion ) number ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = (c1 : ( ( quaternion ) ( quaternion ) number ) .|. c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) - (c2 : ( ( quaternion ) ( quaternion ) number ) .|. c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:59
for c1, c2, c3 being ( ( quaternion ) ( quaternion ) number ) holds c1 : ( ( quaternion ) ( quaternion ) number ) .|. (c2 : ( ( quaternion ) ( quaternion ) number ) - c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = (c1 : ( ( quaternion ) ( quaternion ) number ) .|. c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) - (c1 : ( ( quaternion ) ( quaternion ) number ) .|. c3 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:60
for c1, c2 being ( ( quaternion ) ( quaternion ) number ) holds (c1 : ( ( quaternion ) ( quaternion ) number ) + c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) .|. (c1 : ( ( quaternion ) ( quaternion ) number ) + c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = (((c1 : ( ( quaternion ) ( quaternion ) number ) .|. c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) + (c1 : ( ( quaternion ) ( quaternion ) number ) .|. c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) + (c2 : ( ( quaternion ) ( quaternion ) number ) .|. c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) + (c2 : ( ( quaternion ) ( quaternion ) number ) .|. c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;

theorem :: QUATERN2:61
for c1, c2 being ( ( quaternion ) ( quaternion ) number ) holds (c1 : ( ( quaternion ) ( quaternion ) number ) - c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) .|. (c1 : ( ( quaternion ) ( quaternion ) number ) - c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) = (((c1 : ( ( quaternion ) ( quaternion ) number ) .|. c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) - (c1 : ( ( quaternion ) ( quaternion ) number ) .|. c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) - (c2 : ( ( quaternion ) ( quaternion ) number ) .|. c1 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) + (c2 : ( ( quaternion ) ( quaternion ) number ) .|. c2 : ( ( quaternion ) ( quaternion ) number ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) : ( ( ) ( quaternion ) Element of QUATERNION : ( ( ) ( non zero ) set ) ) ;