quaterni.miz

begin

 reserve a,b,c,d,x,y,w,z,x1,x2,x3,x4,X for set;

 reserve A for non empty set;

 definition

 :: QUATERNI:def1

 func QUATERNION -> set equals ((( Funcs (4, REAL )) \ { x where x be Element of ( Funcs (4, REAL )) : (x . 2) = 0 & (x . 3) = 0 }) \/ COMPLEX );

 coherence ;

 end

 definition

 let x be Number;

 :: QUATERNI:def2

 attr x is quaternion means

 : Def2: x in QUATERNION ;

 end

 registration

 cluster QUATERNION -> non empty;

 coherence ;

 end

 registration

 cluster quaternion for Number;

 existence

 proof

 take the Element of QUATERNION ;

 thus thesis;

 end;

 end

 definition

 mode Quaternion is quaternion Number;

 end

 ::$Canceled

 ::$Canceled



 Lm1: ( 0 ,1,2,3) are_mutually_distinct ;

 theorem :: QUATERNI:5

 {x1, x2, x3, x4} c= X iff x1 in X & x2 in X & x3 in X & x4 in X

 proof



 A1: x1 in {x1, x2, x3, x4} by ENUMSET1:def 2;



 A2: x2 in {x1, x2, x3, x4} by ENUMSET1:def 2;



 A3: x3 in {x1, x2, x3, x4} by ENUMSET1:def 2;

 x4 in {x1, x2, x3, x4} by ENUMSET1:def 2;

 hence {x1, x2, x3, x4} c= X implies x1 in X & x2 in X & x3 in X & x4 in X by A1, A2, A3;

 assume that

 A4: x1 in X and

 A5: x2 in X and

 A6: x3 in X and

 A7: x4 in X;

 let z be object;

 assume z in {x1, x2, x3, x4};

 hence thesis by A4, A5, A6, A7, ENUMSET1:def 2;

 end;

 definition

 let A, x, y, w, z;

 let a,b,c,d be Element of A;

 :: original: -->

 redefine

 func (x,y,w,z) --> (a,b,c,d) -> Function of {x, y, w, z}, A ;

 coherence

 proof

 set f = ((x,y) --> (a,b)), g = ((w,z) --> (c,d)), h = ((x,y,w,z) --> (a,b,c,d));



 A1: ( rng h) c= (( rng f) \/ ( rng g)) by FUNCT_4: 17;



 A2: ( dom h) = {x, y, w, z} by FUNCT_4: 137;

 ( rng h) c= A by A1, XBOOLE_1: 1;

 hence thesis by A2, FUNCT_2:def 1, RELSET_1: 4;

 end;

 end

 definition

 :: QUATERNI:def3

 func <j> -> Number equals (( 0 ,1,2,3) --> ( 0 , 0 ,1, 0 ));

 coherence ;

 :: QUATERNI:def4

 func <k> -> Number equals (( 0 ,1,2,3) --> ( 0 , 0 , 0 ,1));

 coherence ;

 end

 reconsider jj = 1, zz = 0 as Element of REAL by XREAL_0:def 1;



 Lm2: = [*zz, jj*] by ARYTM_0:def 5;

 registration

 cluster -> quaternion;

 coherence by Lm2, XBOOLE_0:def 3;

 cluster <j> -> quaternion;

 coherence

 proof

 set X = { x where x be Element of ( Funcs (4, REAL )) : (x . 2) = 0 & (x . 3) = 0 };

 A1:

 now

 assume <j> in X;

 then ex x be Element of ( Funcs (4, REAL )) st <j> = x & (x . 2) = 0 & (x . 3) = 0 ;

 hence contradiction by FUNCT_4: 140;

 end;

 reconsider z = 0 , j = 0 , w = 1, m = 0 as Element of REAL by XREAL_0:def 1;

 <j> = (( 0 ,1,2,3) --> (z,j,w,m));

 then <j> in ( Funcs (4, REAL )) by CARD_1: 52, FUNCT_2: 8;

 then <j> in (( Funcs (4, REAL )) \ X) by A1, XBOOLE_0:def 5;

 hence <j> in QUATERNION by XBOOLE_0:def 3;

 end;

 cluster <k> -> quaternion;

 coherence

 proof

 set X = { x where x be Element of ( Funcs (4, REAL )) : (x . 2) = 0 & (x . 3) = 0 };

 A2:

 now

 assume <k> in X;

 then ex x be Element of ( Funcs (4, REAL )) st <k> = x & (x . 2) = 0 & (x . 3) = 0 ;

 hence contradiction by FUNCT_4: 139;

 end;

 reconsider z = 0 , j = 0 , w = 0 , m = 1 as Element of REAL by XREAL_0:def 1;

 <k> = (( 0 ,1,2,3) --> (z,j,w,m));

 then <k> in ( Funcs (4, REAL )) by CARD_1: 52, FUNCT_2: 8;

 then <k> in (( Funcs (4, REAL )) \ X) by A2, XBOOLE_0:def 5;

 hence <k> in QUATERNION by XBOOLE_0:def 3;

 end;

 end

 registration

 cluster -> quaternion for Element of QUATERNION ;

 coherence ;

 end

 definition

 let x,y,w,z be Real;

 :: QUATERNI:def5

 func [*x,y,w,z*] -> Element of QUATERNION means

 : Def5: ex x9,y9 be Element of REAL st x9 = x & y9 = y & it = [*x9, y9*] if w = 0 & z = 0

 otherwise it = (( 0 ,1,2,3) --> (x,y,w,z));

 consistency ;

 existence

 proof

 reconsider x9 = x, y9 = y, w9 = w, z9 = z as Element of REAL by XREAL_0:def 1;

 thus w = 0 & z = 0 implies ex t be Element of QUATERNION st ex x9,y9 be Element of REAL st x9 = x & y9 = y & t = [*x9, y9*]

 proof

 assume that w = 0 and z = 0 ;

 set t = [*x9, y9*];

 reconsider t as Element of QUATERNION by XBOOLE_0:def 3;

 take t;

 take x9, y9;

 thus thesis;

 end;

 set e = (( 0 ,1,2,3) --> (x9,y9,w9,z9));

 thus w <> 0 or z <> 0 implies ex t be Element of QUATERNION st t = (( 0 ,1,2,3) --> (x,y,w,z))

 proof

 assume

 A1: w <> 0 or z <> 0 ;



 A2: e in ( Funcs (4, REAL )) by CARD_1: 52, FUNCT_2: 8;

 now

 assume e in { r where r be Element of ( Funcs (4, REAL )) : (r . 2) = 0 & (r . 3) = 0 };

 then ex r be Element of ( Funcs (4, REAL )) st e = r & (r . 2) = 0 & (r . 3) = 0 ;

 hence contradiction by A1, FUNCT_4: 139, FUNCT_4: 140;

 end;

 then e in (( Funcs (4, REAL )) \ { r where r be Element of ( Funcs (4, REAL )) : (r . 2) = 0 & (r . 3) = 0 }) by A2, XBOOLE_0:def 5;

 then

 reconsider e as Element of QUATERNION by XBOOLE_0:def 3;

 take e;

 thus thesis;

 end;

 end;

 uniqueness ;

 end



 Lm3: for x,y be Element of REAL holds [*x, y, 0 , 0 *] = [*x, y*]

 proof

 let x,y be Element of REAL ;

 ex x9,y9 be Element of REAL st (x9 = x) & (y9 = y) & ( [*x, y, 0 , 0 *] = [*x9, y9*]) by Def5;

 hence thesis;

 end;

 ::$Canceled

 theorem :: QUATERNI:7



 Th2: for g be Quaternion holds ex r,s,t,u be Real st g = [*r, s, t, u*]

 proof

 let g be Quaternion;



 A1: g in QUATERNION by Def2;

 per cases ;

 suppose g in COMPLEX ;

 then

 consider r,s be Element of REAL such that

 A2: g = [*r, s*] by ARYTM_0: 9;

 take r, s, 0 , 0 ;

 thus thesis by A2, Def5, A1;

 end;

 suppose not g in COMPLEX ;

 then

 A3: g in (( Funcs (4, REAL )) \ { x where x be Element of ( Funcs (4, REAL )) : (x . 2) = 0 & (x . 3) = 0 }) by A1, XBOOLE_0:def 3;

 then

 consider f be Function such that

 A4: g = f and

 A5: ( dom f) = 4 and

 A6: ( rng f) c= REAL by FUNCT_2:def 2;



 A7: 0 in 4 by CARD_1: 52, ENUMSET1:def 2;



 A8: 1 in 4 by CARD_1: 52, ENUMSET1:def 2;



 A9: 2 in 4 by CARD_1: 52, ENUMSET1:def 2;



 A10: 3 in 4 by CARD_1: 52, ENUMSET1:def 2;



 A11: (f . 0 ) in ( rng f) by A5, A7, FUNCT_1: 3;



 A12: (f . 1) in ( rng f) by A5, A8, FUNCT_1: 3;



 A13: (f . 2) in ( rng f) by A5, A9, FUNCT_1: 3;

 (f . 3) in ( rng f) by A5, A10, FUNCT_1: 3;

 then

 reconsider r = (f . 0 ), s = (f . 1), t = (f . 2), u = (f . 3) as Element of REAL by A6, A11, A12, A13;



 A14: g = (( 0 ,1,2,3) --> (r,s,t,u)) by A4, A5, FUNCT_4: 144, CARD_1: 52;

 take r, s, t, u;

 now

 assume that

 A15: t = 0 and

 A16: u = 0 ;



 A17: ((( 0 ,1,2,3) --> (r,s,t,u)) . 2) = 0 by A15, FUNCT_4: 140;

 ((( 0 ,1,2,3) --> (r,s,t,u)) . 3) = 0 by A16, FUNCT_4: 139;

 then g in { x where x be Element of ( Funcs (4, REAL )) : (x . 2) = 0 & (x . 3) = 0 } by A3, A14, A17;

 hence contradiction by A3, XBOOLE_0:def 5;

 end;

 hence thesis by A14, Def5;

 end;

 end;

 reserve i,j,k for Element of NAT ;

 reserve a,b,c,d for Real;

 reserve y,r,s,x,t,w for Element of RAT+ ;

 ::$Canceled



 Lm4: for x,y,z be object st [x, y] = {z} holds z = {x} & x = y

 proof

 let x,y,z be object;

 assume

 A1: [x, y] = {z};

 then

 A2: {x, y} in {z} by TARSKI:def 2;

 {x} in {z} by A1, TARSKI:def 2;

 hence

 A3: z = {x} by TARSKI:def 1;

 {x, y} = z by A2, TARSKI:def 1;

 hence thesis by A3, ZFMISC_1: 5;

 end;

 theorem :: QUATERNI:9



 Th3: for A be Subset of RAT+ st (ex t st t in A & t <> {} ) & for r, s st r in A & s <=' r holds s in A holds ex r1,r2,r3,r4,r5 be Element of RAT+ st r1 in A & r2 in A & r3 in A & r4 in A & r5 in A & r1 <> r2 & r1 <> r3 & r1 <> r4 & r1 <> r5 & r2 <> r3 & r2 <> r4 & r2 <> r5 & r3 <> r4 & r3 <> r5 & r4 <> r5

 proof

 let A be Subset of RAT+ ;

 given t such that

 A1: t in A and

 A2: t <> {} ;

 assume

 A3: for r, s st r in A & s <=' r holds s in A;

 consider x such that

 A4: t = (x + x) by ARYTM_3: 60;

 consider y such that

 A5: x = (y + y) by ARYTM_3: 60;

 consider w such that

 A6: y = (w + w) by ARYTM_3: 60;

 take {} , w, y, x, t;



 A7: {} <=' t by ARYTM_3: 64;



 A8: x <=' t by A4;



 A9: y <=' x by A5;



 A10: w <=' y by A6;



 A11: y <=' t by A8, A9, ARYTM_3: 67;

 w <=' x by A9, A10, ARYTM_3: 67;

 hence {} in A & w in A & y in A & x in A & t in A by A1, A3, A7, A8, A9, ARYTM_3: 67;



 A12: {} <> x by A2, A4, ARYTM_3: 50;

 then

 A13: {} <> y by A5, ARYTM_3: 50;



 A14: x <> t

 proof

 assume x = t;

 then (t + {} ) = (t + t) by A4, ARYTM_3: 50;

 hence contradiction by A2, ARYTM_3: 62;

 end;



 A15: y <> x

 proof

 assume y = x;

 then (x + {} ) = (x + x) by A5, ARYTM_3: 50;

 hence contradiction by A12, ARYTM_3: 62;

 end;

 w <> y

 proof

 assume w = y;

 then (y + {} ) = (y + y) by A6, ARYTM_3: 50;

 hence contradiction by A13, ARYTM_3: 62;

 end;

 hence thesis by A2, A4, A5, A6, A8, A9, A10, A11, A14, A15, ARYTM_3: 50, ARYTM_3: 66;

 end;



 Lm5: not (( 0 ,1,2,3) --> (a,b,c,d)) in REAL

 proof

 set f = (( 0 ,1,2,3) --> (a,b,c,d));



 A1: f = { [ 0 , a], [1, b], [2, c], [3, d]} by Lm1, FUNCT_4: 145;

 now

 assume f in { [i, j] : (i,j) are_coprime & j <> {} };

 then

 consider i, j such that

 A2: f = [i, j] and (i,j) are_coprime and j <> {} ;



 A3: {i} in f by A2, TARSKI:def 2;



 A4: {i, j} in f by A2, TARSKI:def 2;

 A5:

 now

 assume i = j;

 then {i} = {i, j} by ENUMSET1: 29;

 then

 A6: [i, j] = { {i}} by ENUMSET1: 29;

 then

 A7: [ 0 , a] in { {i}} by A1, A2, ENUMSET1:def 2;



 A8: [1, b] in { {i}} by A1, A2, A6, ENUMSET1:def 2;



 A9: [ 0 , a] = {i} by A7, TARSKI:def 1;

 [1, b] = {i} by A8, TARSKI:def 1;

 hence contradiction by A9, XTUPLE_0: 1;

 end;

 per cases by A1, A3, A4, ENUMSET1:def 2;

 suppose {i} = [ 0 , a] & {i, j} = [ 0 , a];

 hence contradiction by A5, ZFMISC_1: 5;

 end;

 suppose that

 A10: {i} = [ 0 , a] and

 A11: {i, j} = [1, b];



 A12: i = { 0 } by A10, Lm4;

 i in { {1}, {1, b}} by A11, TARSKI:def 2;

 then i = {1, b} or i = {1} by TARSKI:def 2;

 then 1 in i by TARSKI:def 1, TARSKI:def 2;

 hence contradiction by A12, TARSKI:def 1;

 end;

 suppose that

 A13: {i} = [ 0 , a] and

 A14: {i, j} = [2, c];



 A15: i = { 0 } by A13, Lm4;

 i in { {2}, {2, c}} by A14, TARSKI:def 2;

 then i = {2, c} or i = {2} by TARSKI:def 2;

 then 2 in i by TARSKI:def 1, TARSKI:def 2;

 hence contradiction by A15, TARSKI:def 1;

 end;

 suppose that

 A16: {i} = [ 0 , a] and

 A17: {i, j} = [3, d];



 A18: i = { 0 } by A16, Lm4;

 i in { {3}, {3, d}} by A17, TARSKI:def 2;

 then i = {3, d} or i = {3} by TARSKI:def 2;

 then 3 in i by TARSKI:def 1, TARSKI:def 2;

 hence contradiction by A18, TARSKI:def 1;

 end;

 suppose that

 A19: {i} = [1, b] and

 A20: {i, j} = [ 0 , a];



 A21: i = {1} by A19, Lm4;

 i in { { 0 }, { 0 , a}} by A20, TARSKI:def 2;

 then i = { 0 , a} or i = { 0 } by TARSKI:def 2;

 then 0 in i by TARSKI:def 1, TARSKI:def 2;

 hence contradiction by A21, TARSKI:def 1;

 end;

 suppose {i} = [1, b] & {i, j} = [1, b];

 hence contradiction by A5, ZFMISC_1: 5;

 end;

 suppose that

 A22: {i} = [1, b] and

 A23: {i, j} = [2, c];



 A24: i = {1} by A22, Lm4;

 i in { {2}, {2, c}} by A23, TARSKI:def 2;

 then i = {2, c} or i = {2} by TARSKI:def 2;

 then 2 in i by TARSKI:def 1, TARSKI:def 2;

 hence contradiction by A24, TARSKI:def 1;

 end;

 suppose that

 A25: {i} = [1, b] and

 A26: {i, j} = [3, d];



 A27: i = {1} by A25, Lm4;

 i in { {3}, {3, d}} by A26, TARSKI:def 2;

 then i = {3, d} or i = {3} by TARSKI:def 2;

 then 3 in i by TARSKI:def 1, TARSKI:def 2;

 hence contradiction by A27, TARSKI:def 1;

 end;

 suppose that

 A28: {i} = [2, c] and

 A29: {i, j} = [ 0 , a];



 A30: i = {2} by A28, Lm4;

 i in { { 0 }, { 0 , a}} by A29, TARSKI:def 2;

 then i = { 0 , a} or i = { 0 } by TARSKI:def 2;

 then 0 in i by TARSKI:def 1, TARSKI:def 2;

 hence contradiction by A30, TARSKI:def 1;

 end;

 suppose that

 A31: {i} = [2, c] and

 A32: {i, j} = [1, b];



 A33: i = {2} by A31, Lm4;

 i in { {1}, {1, b}} by A32, TARSKI:def 2;

 then i = {1, b} or i = {1} by TARSKI:def 2;

 then 1 in i by TARSKI:def 1, TARSKI:def 2;

 hence contradiction by A33, TARSKI:def 1;

 end;

 suppose {i} = [2, c] & {i, j} = [2, c];

 hence contradiction by A5, ZFMISC_1: 5;

 end;

 suppose that

 A34: {i} = [2, c] and

 A35: {i, j} = [3, d];



 A36: i = {2} by A34, Lm4;

 i in { {3}, {3, d}} by A35, TARSKI:def 2;

 then i = {3, d} or i = {3} by TARSKI:def 2;

 then 3 in i by TARSKI:def 1, TARSKI:def 2;

 hence contradiction by A36, TARSKI:def 1;

 end;

 suppose that

 A37: {i} = [3, d] and

 A38: {i, j} = [ 0 , a];



 A39: i = {3} by A37, Lm4;

 i in { { 0 }, { 0 , a}} by A38, TARSKI:def 2;

 then i = { 0 , a} or i = { 0 } by TARSKI:def 2;

 then 0 in i by TARSKI:def 1, TARSKI:def 2;

 hence contradiction by A39, TARSKI:def 1;

 end;

 suppose that

 A40: {i} = [3, d] and

 A41: {i, j} = [1, b];



 A42: i = {3} by A40, Lm4;

 i in { {1}, {1, b}} by A41, TARSKI:def 2;

 then i = {1, b} or i = {1} by TARSKI:def 2;

 then 1 in i by TARSKI:def 1, TARSKI:def 2;

 hence contradiction by A42, TARSKI:def 1;

 end;

 suppose that

 A43: {i} = [3, d] and

 A44: {i, j} = [2, c];



 A45: i = {3} by A43, Lm4;

 i in { {2}, {2, c}} by A44, TARSKI:def 2;

 then i = {2, c} or i = {2} by TARSKI:def 2;

 then 2 in i by TARSKI:def 1, TARSKI:def 2;

 hence contradiction by A45, TARSKI:def 1;

 end;

 suppose {i} = [3, d] & {i, j} = [3, d];

 hence contradiction by A5, ZFMISC_1: 5;

 end;

 end;

 then

 A46: not f in ({ [i, j] : (i,j) are_coprime & j <> {} } \ the set of all [k, 1]);

 now

 assume f in omega ;

 then f is non empty ordinal;

 then {} in f by ORDINAL3: 8;

 hence contradiction by A1, ENUMSET1:def 2;

 end;

 then

 A47: not f in RAT+ by A46, XBOOLE_0:def 3;

 set IR = { A where A be Subset of RAT+ : for r be Element of RAT+ st r in A holds (for s be Element of RAT+ st s <=' r holds s in A) & ex s be Element of RAT+ st s in A & r < s };

 not ex x,y,z,w be object st { [ 0 , x], [1, y], [2, z], [3, w]} in IR

 proof

 given x,y,z,w be object such that

 A48: { [ 0 , x], [1, y], [2, z], [3, w]} in IR;

 consider A be Subset of RAT+ such that

 A49: { [ 0 , x], [1, y], [2, z], [3, w]} = A and

 A50: for r be Element of RAT+ st r in A holds (for s be Element of RAT+ st s <=' r holds s in A) & ex s be Element of RAT+ st s in A & r < s by A48;



 A51: [ 0 , x] in A by A49, ENUMSET1:def 2;

 for r,s be Element of RAT+ st r in A & s <=' r holds s in A by A50;

 then

 consider r1,r2,r3,r4,r5 be Element of RAT+ such that

 A52: r1 in A and

 A53: r2 in A and

 A54: r3 in A and

 A55: r4 in A and

 A56: r5 in A and

 A57: r1 <> r2 and

 A58: r1 <> r3 and

 A59: r1 <> r4 and

 A60: r1 <> r5 and

 A61: r2 <> r3 and

 A62: r2 <> r4 and

 A63: r2 <> r5 and

 A64: r3 <> r4 and

 A65: r3 <> r5 and

 A66: r4 <> r5 by A51, Th3;



 A67: r1 = [ 0 , x] or r1 = [1, y] or r1 = [2, z] or r1 = [3, w] by A49, A52, ENUMSET1:def 2;



 A68: r2 = [ 0 , x] or r2 = [1, y] or r2 = [2, z] or r2 = [3, w] by A49, A53, ENUMSET1:def 2;



 A69: r3 = [ 0 , x] or r3 = [1, y] or r3 = [2, z] or r3 = [3, w] by A49, A54, ENUMSET1:def 2;

 r4 = [ 0 , x] or r4 = [1, y] or r4 = [2, z] or r4 = [3, w] by A49, A55, ENUMSET1:def 2;

 hence contradiction by A49, A56, A57, A58, A59, A60, A61, A62, A63, A64, A65, A66, A67, A68, A69, ENUMSET1:def 2;

 end;

 then not f in DEDEKIND_CUTS by A1, ARYTM_2:def 1;

 then

 A70: not f in REAL+ by A47, ARYTM_2:def 2, XBOOLE_0:def 3;

 now

 assume f in [: { {} }, REAL+ :];

 then

 consider x,y be object such that

 A71: x in { {} } and y in REAL+ and

 A72: f = [x, y] by ZFMISC_1: 84;



 A73: x = 0 by A71, TARSKI:def 1;

 f = { [ 0 , a], [1, b], [2, c], [3, d]} by Lm1, FUNCT_4: 145;

 then

 A74: [1, b] in f by ENUMSET1:def 2;

 per cases by A72, A73, A74, TARSKI:def 2;

 suppose { {1, b}, {1}} = { 0 };

 then 0 in { {1, b}, {1}} by TARSKI:def 1;

 hence contradiction by TARSKI:def 2;

 end;

 suppose { {1, b}, {1}} = { 0 , y};

 then 0 in { {1, b}, {1}} by TARSKI:def 2;

 hence contradiction by TARSKI:def 2;

 end;

 end;

 hence thesis by A70, NUMBERS:def 1, XBOOLE_0:def 3;

 end;

 theorem :: QUATERNI:10



 Th4: not (( 0 ,1,2,3) --> (a,b,c,d)) in COMPLEX

 proof

 set f = (( 0 ,1,2,3) --> (a,b,c,d));



 A1: not f in REAL by Lm5;

 not f in ( Funcs ( { 0 , 1}, REAL ))

 proof

 assume f in ( Funcs ( { 0 , 1}, REAL ));

 then ( dom f) = { 0 , 1} by FUNCT_2: 92;

 then { 0 , 1, 2, 3} c= { 0 , 1} by FUNCT_4: 137;

 then ( { 0 , 1} \/ {2, 3}) c= { 0 , 1} by ENUMSET1: 5;

 hence contradiction by XBOOLE_1: 11, ZFMISC_1: 22;

 end;

 then not f in (( Funcs ( { 0 , 1}, REAL )) \ { x where x be Element of ( Funcs ( { 0 , 1}, REAL )) : (x . 1) = 0 });

 hence thesis by A1, NUMBERS:def 2, XBOOLE_0:def 3;

 end;

 ::$Canceled

 theorem :: QUATERNI:12



 Th5: for x1,x2,x3,x4,y1,y2,y3,y4 be Real st [*x1, x2, x3, x4*] = [*y1, y2, y3, y4*] holds x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4

 proof

 let x1,x2,x3,x4,y1,y2,y3,y4 be Real such that

 A1: [*x1, x2, x3, x4*] = [*y1, y2, y3, y4*];

 reconsider xx1 = x1, xx2 = x2, yy1 = y1, yy2 = y2 as Element of REAL by XREAL_0:def 1;

 per cases ;

 suppose

 A2: x3 = 0 & x4 = 0 ;

 then

 A3: [*x1, x2, x3, x4*] = [*xx1, xx2*] by Lm3;

 A4:

 now

 assume y3 <> 0 or y4 <> 0 ;

 then [*xx1, xx2*] = (( 0 ,1,2,3) --> (y1,y2,y3,y4)) by A1, A3, Def5;

 hence contradiction by Th4;

 end;

 then [*y1, y2, y3, y4*] = [*yy1, yy2*] by Lm3;

 hence thesis by A1, A2, A3, A4, ARYTM_0: 10;

 end;

 suppose x3 <> 0 or x4 <> 0 ;

 then

 A5: [*y1, y2, y3, y4*] = (( 0 ,1,2,3) --> (x1,x2,x3,x4)) by A1, Def5;

 now

 assume that

 A6: y3 = 0 and

 A7: y4 = 0 ;

 [*y1, y2, y3, y4*] = [*yy1, yy2*] by A6, A7, Lm3;

 hence contradiction by A5, Th4;

 end;

 then [*y1, y2, y3, y4*] = (( 0 ,1,2,3) --> (y1,y2,y3,y4)) by Def5;

 hence thesis by A5, Lm1, FUNCT_4: 146;

 end;

 end;

 definition

 let x,y be Quaternion;

 consider x1,x2,x3,x4 be Real such that

 A1: x = [*x1, x2, x3, x4*] by Th2;

 consider y1,y2,y3,y4 be Real such that

 A2: y = [*y1, y2, y3, y4*] by Th2;

 :: QUATERNI:def6

 func x + y -> Number means

 : Def6: ex x1,x2,x3,x4,y1,y2,y3,y4 be Real st x = [*x1, x2, x3, x4*] & y = [*y1, y2, y3, y4*] & it = [*(x1 + y1), (x2 + y2), (x3 + y3), (x4 + y4)*];

 existence

 proof

 take [*(x1 + y1), (x2 + y2), (x3 + y3), (x4 + y4)*];

 thus thesis by A1, A2;

 end;

 uniqueness

 proof

 let c1,c2 be Number;

 given x1,x2,x3,x4,y1,y2,y3,y4 be Real such that

 A3: x = [*x1, x2, x3, x4*] and

 A4: y = [*y1, y2, y3, y4*] and

 A5: c1 = [*(x1 + y1), (x2 + y2), (x3 + y3), (x4 + y4)*];

 given x19,x29,x39,x49,y19,y29,y39,y49 be Real such that

 A6: x = [*x19, x29, x39, x49*] and

 A7: y = [*y19, y29, y39, y49*] and

 A8: c2 = [*(x19 + y19), (x29 + y29), (x39 + y39), (x49 + y49)*];



 A9: x1 = x19 by A3, A6, Th5;



 A10: x2 = x29 by A3, A6, Th5;



 A11: x3 = x39 by A3, A6, Th5;



 A12: x4 = x49 by A3, A6, Th5;



 A13: y1 = y19 by A4, A7, Th5;



 A14: y2 = y29 by A4, A7, Th5;

 y3 = y39 by A4, A7, Th5;

 hence thesis by A4, A5, A7, A8, A9, A10, A11, A12, A13, A14, Th5;

 end;

 commutativity ;

 end



 Lm6: 0 = [* 0 , 0 , 0 , 0 *]

 proof

 ex x9,y9 be Element of REAL st (x9 = 0 ) & (y9 = 0 ) & ( [* 0 , 0 , 0 , 0 *] = [*x9, y9*]) by Def5;

 hence thesis by ARYTM_0:def 5;

 end;

 definition

 let z be Quaternion;

 consider v,w,x,y be Real such that

 A1: z = [*v, w, x, y*] by Th2;

 :: QUATERNI:def7

 func - z -> Quaternion means

 : Def7: (z + it ) = 0 ;

 existence

 proof

 reconsider z9 = [*( - v), ( - w), ( - x), ( - y)*] as Quaternion;

 take z9;



 A2: 0 = (v + ( - v));



 A3: 0 = (w + ( - w));



 A4: 0 = (x + ( - x));

 0 = (y + ( - y));

 hence thesis by A1, A2, A3, A4, Def6, Lm6;

 end;

 uniqueness

 proof

 let c1,c2 be Quaternion such that

 A5: (z + c1) = 0 and

 A6: (z + c2) = 0 ;

 consider x1,x2,x3,x4,y1,y2,y3,y4 be Real such that

 A7: z = [*x1, x2, x3, x4*] and

 A8: c1 = [*y1, y2, y3, y4*] and

 A9: 0 = [*(x1 + y1), (x2 + y2), (x3 + y3), (x4 + y4)*] by A5, Def6;

 consider x19,x29,x39,x49,y19,y29,y39,y49 be Real such that

 A10: z = [*x19, x29, x39, x49*] and

 A11: c2 = [*y19, y29, y39, y49*] and

 A12: 0 = [*(x19 + y19), (x29 + y29), (x39 + y39), (x49 + y49)*] by A6, Def6;



 A13: x1 = x19 by A7, A10, Th5;



 A14: x2 = x29 by A7, A10, Th5;



 A15: x3 = x39 by A7, A10, Th5;



 A16: x4 = x49 by A7, A10, Th5;



 A17: (x1 + y1) = 0 by A9, Lm6, Th5;



 A18: (x1 + y19) = 0 by A12, A13, Lm6, Th5;



 A19: (x2 + y2) = 0 by A9, Lm6, Th5;



 A20: (x2 + y29) = 0 by A12, A14, Lm6, Th5;



 A21: (x3 + y3) = 0 by A9, Lm6, Th5;



 A22: (x3 + y39) = 0 by A12, A15, Lm6, Th5;



 A23: (x4 + y4) = 0 by A9, Lm6, Th5;

 (x4 + y49) = 0 by A12, A16, Lm6, Th5;

 hence thesis by A8, A11, A17, A18, A19, A20, A21, A22, A23;

 end;

 involutiveness ;

 end

 definition

 let x,y be Quaternion;

 :: QUATERNI:def8

 func x - y -> Number equals (x + ( - y));

 coherence ;

 end

 definition

 let x,y be Quaternion;

 consider x1,x2,x3,x4 be Real such that

 A1: x = [*x1, x2, x3, x4*] by Th2;

 consider y1,y2,y3,y4 be Real such that

 A2: y = [*y1, y2, y3, y4*] by Th2;

 :: QUATERNI:def9

 func x * y -> Number means

 : Def9: ex x1,x2,x3,x4,y1,y2,y3,y4 be Real st x = [*x1, x2, x3, x4*] & y = [*y1, y2, y3, y4*] & it = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)), ((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)), ((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)), ((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*];

 existence

 proof

 take [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)), ((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)), ((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)), ((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*];

 thus thesis by A1, A2;

 end;

 uniqueness

 proof

 let c1,c2 be Number;

 given x1,x2,x3,x4,y1,y2,y3,y4 be Real such that

 A3: x = [*x1, x2, x3, x4*] and

 A4: y = [*y1, y2, y3, y4*] and

 A5: c1 = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)), ((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)), ((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)), ((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*];

 given x19,x29,x39,x49,y19,y29,y39,y49 be Real such that

 A6: x = [*x19, x29, x39, x49*] and

 A7: y = [*y19, y29, y39, y49*] and

 A8: c2 = [*((((x19 * y19) - (x29 * y29)) - (x39 * y39)) - (x49 * y49)), ((((x19 * y29) + (x29 * y19)) + (x39 * y49)) - (x49 * y39)), ((((x19 * y39) + (y19 * x39)) + (y29 * x49)) - (y49 * x29)), ((((x19 * y49) + (x49 * y19)) + (x29 * y39)) - (x39 * y29))*];



 A9: x1 = x19 by A3, A6, Th5;



 A10: x2 = x29 by A3, A6, Th5;



 A11: x3 = x39 by A3, A6, Th5;



 A12: x4 = x49 by A3, A6, Th5;



 A13: y1 = y19 by A4, A7, Th5;



 A14: y2 = y29 by A4, A7, Th5;



 A15: y3 = y39 by A4, A7, Th5;

 y4 = y49 by A4, A7, Th5;

 hence thesis by A5, A8, A9, A10, A11, A12, A13, A14, A15;

 end;

 end

 registration

 let z,z9 be Quaternion;

 cluster (z + z9) -> quaternion;

 coherence

 proof

 ex x1,x2,x3,x4,y1,y2,y3,y4 be Real st z = [*x1, x2, x3, x4*] & z9 = [*y1, y2, y3, y4*] & (z + z9) = [*(x1 + y1), (x2 + y2), (x3 + y3), (x4 + y4)*] by Def6;

 hence thesis;

 end;

 cluster (z * z9) -> quaternion;

 coherence

 proof

 ex x1,x2,x3,x4,y1,y2,y3,y4 be Real st z = [*x1, x2, x3, x4*] & z9 = [*y1, y2, y3, y4*] & (z * z9) = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)), ((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)), ((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)), ((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] by Def9;

 hence (z * z9) in QUATERNION ;

 end;

 end

 definition

 :: original: <j>

 redefine

 :: QUATERNI:def10

 func <j> -> Element of QUATERNION equals [* 0 , 0 , 1, 0 *];

 coherence by Def2;

 compatibility by Def5;

 :: original: <k>

 redefine

 :: QUATERNI:def11

 func <k> -> Element of QUATERNION equals [* 0 , 0 , 0 , 1*];

 coherence by Def2;

 compatibility by Def5;

 end

 theorem :: QUATERNI:13

 ( * ) = ( - 1)

 proof

 = [*zz, jj, zz, zz*] by Lm2, Lm3;



 then

 A1: ( * ) = [*(((( 0 * 0 ) - (1 * 1)) - ( 0 * 0 )) - ( 0 * 0 )), (((( 0 * 1) + (1 * 0 )) + ( 0 * 0 )) - ( 0 * 0 )), (((( 0 * 0 ) + ( 0 * 0 )) + (1 * 0 )) - ( 0 * 1)), (((( 0 * 0 ) + ( 0 * 0 )) + (1 * 0 )) - ( 0 * 1))*] by Def9

 .= [*( - 1), 0 , 0 , 0 *];

 ( - 1) = [*( - jj), zz*] by ARYTM_0:def 5;

 hence thesis by A1, Lm3;

 end;

 theorem :: QUATERNI:14

 ( <j> * <j> ) = ( - 1)

 proof



 A1: ( <j> * <j> ) = [*(((( 0 * 0 ) - ( 0 * 0 )) - (1 * 1)) - ( 0 * 0 )), (((( 0 * 0 ) + ( 0 * 0 )) + ( 0 * 0 )) - ( 0 * 1)), (((( 0 * 1) + ( 0 * 1)) + ( 0 * 0 )) - ( 0 * 0 )), (((( 0 * 0 ) + ( 0 * 0 )) + ( 0 * 1)) - (1 * 0 ))*] by Def9

 .= [*( - 1), 0 , 0 , 0 *];

 [*( - 1), 0 , 0 , 0 *] = [*( - jj), zz*] by Lm3;

 hence thesis by A1, ARYTM_0:def 5;

 end;

 theorem :: QUATERNI:15

 ( <k> * <k> ) = ( - 1)

 proof



 A1: ( <k> * <k> ) = [*(((( 0 * 0 ) - ( 0 * 0 )) - ( 0 * 0 )) - (1 * 1)), (((( 0 * 0 ) + ( 0 * 0 )) + ( 0 * 1)) - (1 * 0 )), (((( 0 * 0 ) + ( 0 * 0 )) + ( 0 * 1)) - (1 * 0 )), (((( 0 * 1) + (1 * 0 )) + ( 0 * 0 )) - ( 0 * 0 ))*] by Def9

 .= [*( - 1), 0 , 0 , 0 *];

 ( - 1) = [*( - jj), zz*] by ARYTM_0:def 5;

 hence thesis by A1, Lm3;

 end;

 theorem :: QUATERNI:16

 ( * <j> ) = <k>

 proof

 = [* 0 , 1, 0 , 0 *] by Lm2, Lm3;



 then ( * <j> ) = [*(((( 0 * 0 ) - (1 * 0 )) - ( 0 * 1)) - ( 0 * 0 )), (((( 0 * 0 ) + (1 * 0 )) + ( 0 * 0 )) - ( 0 * 1)), (((( 0 * 1) + ( 0 * 0 )) + ( 0 * 0 )) - ( 0 * 1)), (((( 0 * 0 ) + ( 0 * 0 )) + (1 * 1)) - ( 0 * 0 ))*] by Def9

 .= [* 0 , 0 , 0 , 1*];

 hence thesis;

 end;

 theorem :: QUATERNI:17

 ( <j> * <k> ) = 

 proof

 ( <j> * <k> ) = [*(((( 0 * 0 ) - ( 0 * 0 )) - (1 * 0 )) - ( 0 * 1)), (((( 0 * 0 ) + ( 0 * 0 )) + (1 * 1)) - ( 0 * 0 )), (((( 0 * 0 ) + ( 0 * 1)) + ( 0 * 0 )) - (1 * 0 )), (((( 0 * 1) + ( 0 * 0 )) + ( 0 * 0 )) - (1 * 0 ))*] by Def9

 .= [* 0 , 1, 0 , 0 *];

 hence thesis by Lm2, Lm3;

 end;

 theorem :: QUATERNI:18

 ( <k> * ) = <j>

 proof

 = [* 0 , 1, 0 , 0 *] by Lm2, Lm3;



 then ( <k> * ) = [*(((( 0 * 0 ) - ( 0 * 1)) - ( 0 * 0 )) - (1 * 0 )), (((( 0 * 1) + ( 0 * 0 )) + ( 0 * 0 )) - (1 * 0 )), (((( 0 * 0 ) + ( 0 * 0 )) + (1 * 1)) - ( 0 * 0 )), (((( 0 * 0 ) + (1 * 0 )) + ( 0 * 0 )) - ( 0 * 1))*] by Def9

 .= [* 0 , 0 , 1, 0 *];

 hence thesis;

 end;

 theorem :: QUATERNI:19

 ( * <j> ) = ( - ( <j> * ))

 proof



 A1: = [*zz, jj, zz, zz*] by Lm2, Lm3;



 then

 A2: ( * <j> ) = [*(((( 0 * 0 ) - (1 * 0 )) - ( 0 * 1)) - ( 0 * 0 )), (((( 0 * 0 ) + (1 * 0 )) + ( 0 * 0 )) - ( 0 * 1)), (((( 0 * 1) + ( 0 * 0 )) + ( 0 * 0 )) - ( 0 * 1)), (((( 0 * 0 ) + ( 0 * 0 )) + (1 * 1)) - ( 0 * 0 ))*] by Def9

 .= [*zz, zz, zz, jj*];

 ( <j> * ) = [*(((( 0 * 0 ) - ( 0 * 1)) - (1 * 0 )) - ( 0 * 0 )), (((( 0 * 1) + ( 0 * 0 )) + (1 * 0 )) - ( 0 * 0 )), (((( 0 * 0 ) + ( 0 * 1)) + (1 * 0 )) - ( 0 * 0 )), (((( 0 * 0 ) + ( 0 * 0 )) + ( 0 * 0 )) - (1 * 1))*] by A1, Def9

 .= [*zz, zz, zz, ( - jj)*];



 then (( * <j> ) + ( <j> * )) = [*( 0 + 0 ), ( 0 + 0 ), ( 0 + 0 ), (1 + ( - 1))*] by A2, Def6

 .= 0 by Lm6;

 hence thesis by Def7;

 end;

 theorem :: QUATERNI:20

 ( <j> * <k> ) = ( - ( <k> * <j> ))

 proof



 A1: ( <j> * <k> ) = [*(((( 0 * 0 ) - ( 0 * 0 )) - (1 * 0 )) - ( 0 * 1)), (((( 0 * 0 ) + ( 0 * 0 )) + (1 * 1)) - ( 0 * 0 )), (((( 0 * 0 ) + ( 0 * 1)) + ( 0 * 0 )) - (1 * 0 )), (((( 0 * 1) + ( 0 * 0 )) + ( 0 * 0 )) - (1 * 0 ))*] by Def9

 .= [*zz, jj, zz, zz*];

 ( <k> * <j> ) = [*(((( 0 * 0 ) - ( 0 * 0 )) - ( 0 * 1)) - (1 * 0 )), (((( 0 * 0 ) + ( 0 * 0 )) + ( 0 * 0 )) - (1 * 1)), (((( 0 * 1) + ( 0 * 0 )) + ( 0 * 1)) - ( 0 * 0 )), (((( 0 * 0 ) + (1 * 0 )) + ( 0 * 1)) - ( 0 * 0 ))*] by Def9

 .= [*zz, ( - jj), zz, zz*];



 then (( <j> * <k> ) + ( <k> * <j> )) = [*( 0 + 0 ), ( 0 + 0 ), ( 0 + 0 ), (1 + ( - 1))*] by A1, Def6

 .= 0 by Lm6;

 hence thesis by Def7;

 end;

 theorem :: QUATERNI:21

 ( <k> * ) = ( - ( * <k> ))

 proof



 A1: = [*zz, jj, zz, zz*] by Lm2, Lm3;



 then

 A2: ( <k> * ) = [*(((( 0 * 0 ) - ( 0 * 1)) - ( 0 * 0 )) - (1 * 0 )), (((( 0 * 1) + ( 0 * 0 )) + ( 0 * 0 )) - (1 * 0 )), (((( 0 * 0 ) + ( 0 * 0 )) + (1 * 1)) - ( 0 * 0 )), (((( 0 * 0 ) + (1 * 0 )) + ( 0 * 0 )) - ( 0 * 1))*] by Def9

 .= [*zz, zz, jj, zz*];

 ( * <k> ) = [*(((( 0 * 0 ) - (1 * 0 )) - ( 0 * 0 )) - ( 0 * 1)), (((( 0 * 0 ) + (1 * 0 )) + ( 0 * 1)) - ( 0 * 0 )), (((( 0 * 0 ) + ( 0 * 0 )) + ( 0 * 1)) - (1 * 1)), (((( 0 * 1) + ( 0 * 0 )) + (1 * 0 )) - ( 0 * 0 ))*] by A1, Def9

 .= [*zz, zz, ( - jj), zz*];



 then (( <k> * ) + ( * <k> )) = [*( 0 + 0 ), ( 0 + 0 ), (1 + ( - 1)), ( 0 + 0 )*] by A2, Def6

 .= 0 by Lm6;

 hence thesis by Def7;

 end;

 definition

 let z be Quaternion;

 :: QUATERNI:def12

 func Rea z -> Number means

 : Def12: ex z9 be Complex st z = z9 & it = ( Re z9) if z in COMPLEX

 otherwise ex f be Function of 4, REAL st z = f & it = (f . 0 );

 existence

 proof

 thus z in COMPLEX implies ex IT be Number, z9 be Complex st z = z9 & IT = ( Re z9)

 proof

 assume z in COMPLEX ;

 then

 consider r,s be Element of REAL such that

 A1: z = [*r, s*] by ARYTM_0: 9;

 set z9 = [*r, s*];

 take ( Re z9), z9;

 thus thesis by A1;

 end;

 assume

 A2: not z in COMPLEX ;

 z in QUATERNION by Def2;

 then z in (( Funcs (4, REAL )) \ { x where x be Element of ( Funcs (4, REAL )) : (x . 2) = 0 & (x . 3) = 0 }) by A2, XBOOLE_0:def 3;

 then

 reconsider f = z as Function of 4, REAL by FUNCT_2: 66;

 take (f . 0 ), f;

 thus thesis;

 end;

 uniqueness ;

 consistency ;

 :: QUATERNI:def13

 func Im1 z -> Number means

 : Def13: ex z9 be Complex st z = z9 & it = ( Im z9) if z in COMPLEX

 otherwise ex f be Function of 4, REAL st z = f & it = (f . 1);

 existence

 proof

 thus z in COMPLEX implies ex IT be Number, z9 be Complex st z = z9 & IT = ( Im z9)

 proof

 assume z in COMPLEX ;

 then

 consider r,s be Element of REAL such that

 A3: z = [*r, s*] by ARYTM_0: 9;

 set z9 = [*r, s*];

 take ( Im z9), z9;

 thus thesis by A3;

 end;

 assume

 A4: not z in COMPLEX ;

 z in QUATERNION by Def2;

 then z in (( Funcs (4, REAL )) \ { x where x be Element of ( Funcs (4, REAL )) : (x . 2) = 0 & (x . 3) = 0 }) by A4, XBOOLE_0:def 3;

 then

 reconsider f = z as Function of 4, REAL by FUNCT_2: 66;

 take (f . 1), f;

 thus thesis;

 end;

 uniqueness ;

 consistency ;

 :: QUATERNI:def14

 func Im2 z -> Number means

 : Def14: it = 0 if z in COMPLEX

 otherwise ex f be Function of 4, REAL st z = f & it = (f . 2);

 existence

 proof

 thus z in COMPLEX implies ex IT be Number st IT = 0 ;

 assume

 A5: not z in COMPLEX ;

 z in QUATERNION by Def2;

 then z in (( Funcs (4, REAL )) \ { x where x be Element of ( Funcs (4, REAL )) : (x . 2) = 0 & (x . 3) = 0 }) by A5, XBOOLE_0:def 3;

 then

 reconsider f = z as Function of 4, REAL by FUNCT_2: 66;

 take (f . 2), f;

 thus thesis;

 end;

 uniqueness ;

 consistency ;

 :: QUATERNI:def15

 func Im3 z -> Number means

 : Def15: it = 0 if z in COMPLEX

 otherwise ex f be Function of 4, REAL st z = f & it = (f . 3);

 existence

 proof

 thus z in COMPLEX implies ex IT be Number st IT = 0 ;

 assume

 A6: not z in COMPLEX ;

 z in QUATERNION by Def2;

 then z in (( Funcs (4, REAL )) \ { x where x be Element of ( Funcs (4, REAL )) : (x . 2) = 0 & (x . 3) = 0 }) by A6, XBOOLE_0:def 3;

 then

 reconsider f = z as Function of 4, REAL by FUNCT_2: 66;

 take (f . 3), f;

 thus thesis;

 end;

 uniqueness ;

 consistency ;

 end

 registration

 let z be Quaternion;

 cluster ( Rea z) -> real;

 coherence

 proof

 per cases ;

 suppose z in COMPLEX ;

 then ex z9 be Complex st (z = z9) & (( Rea z) = ( Re z9)) by Def12;

 hence thesis;

 end;

 suppose not z in COMPLEX ;

 then ex f be Function of 4, REAL st (z = f) & (( Rea z) = (f . 0 )) by Def12;

 hence thesis;

 end;

 end;

 cluster ( Im1 z) -> real;

 coherence

 proof

 per cases ;

 suppose z in COMPLEX ;

 then ex z9 be Complex st (z = z9) & (( Im1 z) = ( Im z9)) by Def13;

 hence thesis;

 end;

 suppose not z in COMPLEX ;

 then ex f be Function of 4, REAL st (z = f) & (( Im1 z) = (f . 1)) by Def13;

 hence thesis;

 end;

 end;

 cluster ( Im2 z) -> real;

 coherence

 proof

 per cases ;

 suppose z in COMPLEX ;

 hence thesis by Def14;

 end;

 suppose not z in COMPLEX ;

 then ex f be Function of 4, REAL st (z = f) & (( Im2 z) = (f . 2)) by Def14;

 hence thesis;

 end;

 end;

 cluster ( Im3 z) -> real;

 coherence

 proof

 per cases ;

 suppose z in COMPLEX ;

 hence thesis by Def15;

 end;

 suppose not z in COMPLEX ;

 then ex f be Function of 4, REAL st (z = f) & (( Im3 z) = (f . 3)) by Def15;

 hence thesis;

 end;

 end;

 end

 theorem :: QUATERNI:22



 Th15: for f be Function of 4, REAL holds ex a, b, c, d st f = (( 0 ,1,2,3) --> (a,b,c,d))

 proof

 let f be Function of 4, REAL ;

 reconsider a = (f . 0 ), b = (f . 1), c = (f . 2), d = (f . 3) as Element of REAL by XREAL_0:def 1;

 take a, b, c, d;

 ( dom f) = { 0 , 1, 2, 3} by CARD_1: 52, FUNCT_2:def 1;

 hence thesis by FUNCT_4: 144;

 end;



 Lm7: for a,b be Element of REAL holds ( Re [*a, b*]) = a & ( Im [*a, b*]) = b

 proof

 let a,b be Element of REAL ;

 reconsider a9 = a, b9 = b as Element of REAL ;

 thus ( Re [*a, b*]) = a

 proof

 per cases ;

 suppose b = 0 ;

 then [*a, b*] = a by ARYTM_0:def 5;

 hence thesis by COMPLEX1:def 1;

 end;

 suppose b <> 0 ;

 then

 A1: [*a, b*] = (( 0 ,1) --> (a9,b9)) by ARYTM_0:def 5;

 then

 reconsider f = [*a, b*] as Function of 2, REAL by CARD_1: 50;

 not [*a, b*] in REAL by A1, ARYTM_0: 8;

 then

 a2: not [*a, b*] is real by XREAL_0:def 1;

 (f . 0 ) = a by A1, FUNCT_4: 63;

 hence thesis by a2, COMPLEX1:def 1;

 end;

 end;

 per cases ;

 suppose

 A3: b = 0 ;

 then [*a, b*] = a by ARYTM_0:def 5;

 hence thesis by A3, COMPLEX1:def 2;

 end;

 suppose b <> 0 ;

 then

 A4: [*a, b*] = (( 0 ,1) --> (a9,b9)) by ARYTM_0:def 5;

 then

 reconsider f = [*a, b*] as Function of 2, REAL by CARD_1: 50;

 not [*a, b*] in REAL by A4, ARYTM_0: 8;

 then

 a5: not [*a, b*] is real by XREAL_0:def 1;

 (f . 1) = b by A4, FUNCT_4: 63;

 hence thesis by a5, COMPLEX1:def 2;

 end;

 end;



 Lm8: for z be Complex holds [*( Re z), ( Im z)*] = z

 proof

 let z be Complex;



 A1: z in COMPLEX by XCMPLX_0:def 2;

 per cases ;

 suppose

 A2: z in REAL ;

 then ( Im z) = 0 by COMPLEX1:def 2;



 hence [*( Re z), ( Im z)*] = ( Re z) by ARYTM_0:def 5

 .= z by A2, COMPLEX1:def 1;

 end;

 suppose

 A3: not z in REAL ;

 then

 a3: not z is real by XREAL_0:def 1;

 then

 A4: ex f be Function of 2, REAL st (z = f) & (( Im z) = (f . 1)) by COMPLEX1:def 2;



 A5: ex f be Function of 2, REAL st (z = f) & (( Re z) = (f . 0 )) by a3, COMPLEX1:def 1;

 consider a,b be Element of REAL such that

 A6: z = (( 0 ,1) --> (a,b)) by A4, COMPLEX1: 2;



 A7: ( Re z) = a by A5, A6, FUNCT_4: 63;



 A8: ( Im z) = b by A4, A6, FUNCT_4: 63;

 z in (( Funcs (2, REAL )) \ { x where x be Element of ( Funcs (2, REAL )) : (x . 1) = 0 }) by A1, A3, CARD_1: 50, NUMBERS:def 2, XBOOLE_0:def 3;

 then

 A9: not z in { x where x be Element of ( Funcs (2, REAL )) : (x . 1) = 0 } by XBOOLE_0:def 5;

 reconsider f = z as Element of ( Funcs (2, REAL )) by A6, CARD_1: 50, FUNCT_2: 8;

 (f . 1) <> 0 by A9;

 then b <> 0 by A6, FUNCT_4: 63;

 hence thesis by A6, A7, A8, ARYTM_0:def 5;

 end;

 end;

 theorem :: QUATERNI:23



 Th16: ( Rea [*a, b, c, d*]) = a & ( Im1 [*a, b, c, d*]) = b & ( Im2 [*a, b, c, d*]) = c & ( Im3 [*a, b, c, d*]) = d

 proof

 reconsider aa = a, bb = b, c9 = c, d9 = d as Element of REAL by XREAL_0:def 1;

 thus ( Rea [*a, b, c, d*]) = a

 proof

 per cases ;

 suppose c = 0 & d = 0 ;

 then

 A1: [*a, b, c, d*] = [*aa, bb*] by Lm3;

 ( Re [*aa, bb*]) = a by Lm7;

 hence thesis by A1, Def12;

 end;

 suppose c <> 0 or d <> 0 ;

 then

 A2: [*a, b, c, d*] = (( 0 ,1,2,3) --> (aa,bb,c9,d9)) by Def5;

 then

 reconsider f = [*a, b, c, d*] as Function of 4, REAL by CARD_1: 52;



 A3: not [*a, b, c, d*] in COMPLEX by A2, Th4;

 (f . 0 ) = a by A2, FUNCT_4: 142;

 hence thesis by A3, Def12;

 end;

 end;

 thus ( Im1 [*a, b, c, d*]) = b

 proof

 per cases ;

 suppose c = 0 & d = 0 ;

 then

 A4: [*a, b, c, d*] = [*aa, bb*] by Lm3;

 ( Im [*aa, bb*]) = b by Lm7;

 hence thesis by A4, Def13;

 end;

 suppose c <> 0 or d <> 0 ;

 then

 A5: [*a, b, c, d*] = (( 0 ,1,2,3) --> (aa,bb,c9,d9)) by Def5;

 then

 reconsider f = [*a, b, c, d*] as Function of 4, REAL by CARD_1: 52;



 A6: not [*a, b, c, d*] in COMPLEX by A5, Th4;

 (f . 1) = b by A5, FUNCT_4: 141;

 hence thesis by A6, Def13;

 end;

 end;

 thus ( Im2 [*a, b, c, d*]) = c

 proof

 per cases ;

 suppose

 A7: c = 0 & d = 0 ;

 then [*a, b, c, d*] = [*aa, bb*] by Lm3;

 hence thesis by A7, Def14;

 end;

 suppose c <> 0 or d <> 0 ;

 then

 A8: [*a, b, c, d*] = (( 0 ,1,2,3) --> (aa,bb,c9,d9)) by Def5;

 then

 reconsider f = [*a, b, c, d*] as Function of 4, REAL by CARD_1: 52;



 A9: not [*a, b, c, d*] in COMPLEX by A8, Th4;

 (f . 2) = c by A8, FUNCT_4: 140;

 hence thesis by A9, Def14;

 end;

 end;

 per cases ;

 suppose

 A10: c = 0 & d = 0 ;

 then [*a, b, c, d*] = [*aa, bb*] by Lm3;

 hence thesis by A10, Def15;

 end;

 suppose c <> 0 or d <> 0 ;

 then

 A11: [*a, b, c, d*] = (( 0 ,1,2,3) --> (aa,bb,c9,d9)) by Def5;

 then

 reconsider f = [*a, b, c, d*] as Function of 4, REAL by CARD_1: 52;



 A12: not [*a, b, c, d*] in COMPLEX by A11, Th4;

 (f . 3) = d by A11, FUNCT_4: 139;

 hence thesis by A12, Def15;

 end;

 end;

 reserve z,z1,z2,z3,z4 for Quaternion;

 theorem :: QUATERNI:24



 Th17: z = [*( Rea z), ( Im1 z), ( Im2 z), ( Im3 z)*]

 proof



 A1: z in QUATERNION by Def2;

 per cases ;

 suppose

 A2: z in COMPLEX ;

 then

 A3: ( Im2 z) = 0 by Def14;



 A4: ( Im3 z) = 0 by A2, Def15;



 A5: ex z9 be Complex st (z = z9) & (( Rea z) = ( Re z9)) by A2, Def12;

 consider z9 be Complex such that

 A6: z = z9 and

 A7: ( Im1 z) = ( Im z9) by A2, Def13;

 reconsider Rz = ( Rea z), Imz = ( Im1 z) as Element of REAL by XREAL_0:def 1;

 [*Rz, Imz*] = z9 by A5, A6, A7, Lm8;

 hence thesis by A3, A4, A6, Lm3;

 end;

 suppose

 A8: not z in COMPLEX ;

 then

 A9: ex f be Function of 4, REAL st (z = f) & (( Im1 z) = (f . 1)) by Def13;



 A10: ex f be Function of 4, REAL st (z = f) & (( Rea z) = (f . 0 )) by A8, Def12;



 A11: ex f be Function of 4, REAL st (z = f) & (( Im2 z) = (f . 2)) by A8, Def14;



 A12: ex f be Function of 4, REAL st (z = f) & (( Im3 z) = (f . 3)) by A8, Def15;

 consider a,b,c,d be Real such that

 A13: z = (( 0 ,1,2,3) --> (a,b,c,d)) by A9, Th15;

 reconsider a, b, c, d as Element of REAL by XREAL_0:def 1;



 A14: z = (( 0 ,1,2,3) --> (a,b,c,d)) by A13;



 A15: ( Rea z) = a by A10, A14, FUNCT_4: 142;



 A16: ( Im1 z) = b by A9, A14, FUNCT_4: 141;



 A17: ( Im2 z) = c by A11, A14, FUNCT_4: 140;



 A18: ( Im3 z) = d by A12, A14, FUNCT_4: 139;

 z in (( Funcs (4, REAL )) \ { x where x be Element of ( Funcs (4, REAL )) : (x . 2) = 0 & (x . 3) = 0 }) by A1, A8, XBOOLE_0:def 3;

 then

 A19: not z in { x where x be Element of ( Funcs (4, REAL )) : (x . 2) = 0 & (x . 3) = 0 } by XBOOLE_0:def 5;

 reconsider f = z as Element of ( Funcs (4, REAL )) by A14, CARD_1: 52, FUNCT_2: 8;

 (f . 2) <> 0 or (f . 3) <> 0 by A19;

 then c <> 0 or d <> 0 by A14, FUNCT_4: 139, FUNCT_4: 140;

 hence thesis by A14, A15, A16, A17, A18, Def5;

 end;

 end;

 theorem :: QUATERNI:25



 Th18: ( Rea z1) = ( Rea z2) & ( Im1 z1) = ( Im1 z2) & ( Im2 z1) = ( Im2 z2) & ( Im3 z1) = ( Im3 z2) implies z1 = z2

 proof

 assume that

 A1: ( Rea z1) = ( Rea z2) and

 A2: ( Im1 z1) = ( Im1 z2) and

 A3: ( Im2 z1) = ( Im2 z2) and

 A4: ( Im3 z1) = ( Im3 z2);



 thus z1 = [*( Rea z2), ( Im1 z2), ( Im2 z2), ( Im3 z2)*] by A1, A2, A3, A4, Th17

 .= z2 by Th17;

 end;

 definition

 :: QUATERNI:def16

 func 0q -> Quaternion equals 0 ;

 coherence by Lm6;

 :: QUATERNI:def17

 func 1q -> Quaternion equals 1;

 coherence

 proof

 [*1, 0 , 0 , 0 *] = [*jj, zz*] by Lm3;

 hence thesis by ARYTM_0:def 5;

 end;

 end



 Lm9: for a,b,c,d be Real st ((((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 )) = 0 holds a = 0 & b = 0 & c = 0 & d = 0

 proof

 let a,b,c,d be Real;

 assume

 A1: ((((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 )) = 0 ;



 A2: 0 <= (a ^2 ) by XREAL_1: 63;



 A3: 0 <= (b ^2 ) by XREAL_1: 63;



 A4: 0 <= (c ^2 ) by XREAL_1: 63;



 A5: 0 <= (d ^2 ) by XREAL_1: 63;

 assume

 A6: a <> 0 or b <> 0 or c <> 0 or d <> 0 ;

 per cases by A6;

 suppose a <> 0 ;

 then 0 < ((a ^2 ) + (b ^2 )) by A3, SQUARE_1: 12, XREAL_1: 34;

 hence contradiction by A1, A4, A5;

 end;

 suppose b <> 0 ;

 then 0 < ((a ^2 ) + (b ^2 )) by A2, SQUARE_1: 12, XREAL_1: 34;

 hence contradiction by A1, A4, A5;

 end;

 suppose c <> 0 ;

 then 0 < ((c ^2 ) + (d ^2 )) by A5, SQUARE_1: 12, XREAL_1: 34;

 then 0 < (((a ^2 ) + (b ^2 )) + ((c ^2 ) + (d ^2 ))) by A2, A3;

 hence contradiction by A1;

 end;

 suppose d <> 0 ;

 then 0 < ((c ^2 ) + (d ^2 )) by A4, SQUARE_1: 12, XREAL_1: 34;

 then 0 < (((a ^2 ) + (b ^2 )) + ((c ^2 ) + (d ^2 ))) by A2, A3;

 hence contradiction by A1;

 end;

 end;

 theorem :: QUATERNI:26



 Th19: ( Rea z) = 0 & ( Im1 z) = 0 & ( Im2 z) = 0 & ( Im3 z) = 0 implies z = 0q

 proof

 assume that

 A1: ( Rea z) = 0 and

 A2: ( Im1 z) = 0 and

 A3: ( Im2 z) = 0 and

 A4: ( Im3 z) = 0 ;



 A5: ( Rea z) = ( Rea [* 0 , 0 , 0 , 0 *]) by A1, Th16;



 A6: ( Im1 z) = ( Im1 [* 0 , 0 , 0 , 0 *]) by A2, Th16;



 A7: ( Im2 z) = ( Im2 [* 0 , 0 , 0 , 0 *]) by A3, Th16;

 ( Im3 z) = ( Im3 [* 0 , 0 , 0 , 0 *]) by A4, Th16;

 hence thesis by A5, A6, A7, Lm6, Th18;

 end;

 theorem :: QUATERNI:27

 z = 0 implies ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )) = 0

 proof

 assume

 A1: z = 0 ;

 then

 A2: ( Rea z) = 0 by Lm6, Th16;



 A3: ( Im1 z) = 0 by A1, Lm6, Th16;

 ( Im2 z) = 0 by A1, Lm6, Th16;

 hence thesis by A1, A2, A3, Lm6, Th16;

 end;

 theorem :: QUATERNI:28

 ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )) = 0 implies z = 0q

 proof

 assume

 A1: ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )) = 0 ;

 then

 A2: ( Rea z) = 0 by Lm9;



 A3: ( Im1 z) = 0 by A1, Lm9;



 A4: ( Im2 z) = 0 by A1, Lm9;

 ( Im3 z) = 0 by A1, Lm9;

 hence thesis by A2, A3, A4, Th19;

 end;



 Lm10: [*jj, zz, zz, zz*] = 1

 proof

 [*1, 0 , 0 , 0 *] = [*jj, zz*] by Lm3;

 hence thesis by ARYTM_0:def 5;

 end;

 theorem :: QUATERNI:29

 ( Rea 1q ) = 1 & ( Im1 1q ) = 0 & ( Im2 1q ) = 0 & ( Im3 1q ) = 0 by Lm10, Th16;

 theorem :: QUATERNI:30



 Th23: ( Rea ) = 0 & ( Im1 ) = 1 & ( Im2 ) = 0 & ( Im3 ) = 0

 proof

 [*zz, jj*] = [* 0 , 1, 0 , 0 *] by Lm3;

 hence thesis by Lm2, Th16;

 end;

 theorem :: QUATERNI:31



 Th24: ( Rea <j> ) = 0 & ( Im1 <j> ) = 0 & ( Im2 <j> ) = 1 & ( Im3 <j> ) = 0 & ( Rea <k> ) = 0 & ( Im1 <k> ) = 0 & ( Im2 <k> ) = 0 & ( Im3 <k> ) = 1 by Th16;



 Lm11: for m,n,x,y,z be Quaternion st z = (((m + n) + x) + y) holds ( Rea z) = (((( Rea m) + ( Rea n)) + ( Rea x)) + ( Rea y)) & ( Im1 z) = (((( Im1 m) + ( Im1 n)) + ( Im1 x)) + ( Im1 y)) & ( Im2 z) = (((( Im2 m) + ( Im2 n)) + ( Im2 x)) + ( Im2 y)) & ( Im3 z) = (((( Im3 m) + ( Im3 n)) + ( Im3 x)) + ( Im3 y))

 proof

 let m,n,x,y,z be Quaternion such that

 A1: z = (((m + n) + x) + y);

 consider m1,m2,m3,m4,n1,n2,n3,n4 be Real such that

 A2: m = [*m1, m2, m3, m4*] and

 A3: n = [*n1, n2, n3, n4*] and

 A4: (m + n) = [*(m1 + n1), (m2 + n2), (m3 + n3), (m4 + n4)*] by Def6;

 consider x1,x2,x3,x4,y1,y2,y3,y4 be Real such that

 A5: x = [*x1, x2, x3, x4*] and

 A6: y = [*y1, y2, y3, y4*] and (x + y) = [*(x1 + y1), (x2 + y2), (x3 + y3), (x4 + y4)*] by Def6;



 A7: ( Rea m) = m1 by A2, Th16;



 A8: ( Rea n) = n1 by A3, Th16;



 A9: ( Rea x) = x1 by A5, Th16;



 A10: ( Rea y) = y1 by A6, Th16;



 A11: ( Im1 m) = m2 by A2, Th16;



 A12: ( Im1 n) = n2 by A3, Th16;



 A13: ( Im1 x) = x2 by A5, Th16;



 A14: ( Im1 y) = y2 by A6, Th16;



 A15: ( Im2 m) = m3 by A2, Th16;



 A16: ( Im2 n) = n3 by A3, Th16;



 A17: ( Im2 x) = x3 by A5, Th16;



 A18: ( Im2 y) = y3 by A6, Th16;



 A19: ( Im3 m) = m4 by A2, Th16;



 A20: ( Im3 n) = n4 by A3, Th16;



 A21: ( Im3 x) = x4 by A5, Th16;



 A22: ( Im3 y) = y4 by A6, Th16;

 ((m + n) + x) = [*((m1 + n1) + x1), ((m2 + n2) + x2), ((m3 + n3) + x3), ((m4 + n4) + x4)*] by A4, A5, Def6;

 then z = [*(((m1 + n1) + x1) + y1), (((m2 + n2) + x2) + y2), (((m3 + n3) + x3) + y3), (((m4 + n4) + x4) + y4)*] by A1, A6, Def6;

 hence thesis by A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, Th16;

 end;



 Lm12: for x,y,z be Quaternion st z = (x + y) holds ( Rea z) = (( Rea x) + ( Rea y)) & ( Im1 z) = (( Im1 x) + ( Im1 y)) & ( Im2 z) = (( Im2 x) + ( Im2 y)) & ( Im3 z) = (( Im3 x) + ( Im3 y))

 proof

 let x,y,z be Quaternion such that

 A1: z = (x + y);

 consider x1,x2,x3,x4,y1,y2,y3,y4 be Real such that

 A2: x = [*x1, x2, x3, x4*] and

 A3: y = [*y1, y2, y3, y4*] and

 A4: (x + y) = [*(x1 + y1), (x2 + y2), (x3 + y3), (x4 + y4)*] by Def6;



 A5: ( Rea x) = x1 by A2, Th16;



 A6: ( Rea y) = y1 by A3, Th16;



 A7: ( Im1 x) = x2 by A2, Th16;



 A8: ( Im1 y) = y2 by A3, Th16;



 A9: ( Im2 x) = x3 by A2, Th16;



 A10: ( Im2 y) = y3 by A3, Th16;



 A11: ( Im3 x) = x4 by A2, Th16;

 ( Im3 y) = y4 by A3, Th16;

 hence thesis by A1, A4, A5, A6, A7, A8, A9, A10, A11, Th16;

 end;



 Lm13: (z1 + z2) = [*(( Rea z1) + ( Rea z2)), (( Im1 z1) + ( Im1 z2)), (( Im2 z1) + ( Im2 z2)), (( Im3 z1) + ( Im3 z2))*]

 proof

 set z = [*(( Rea z1) + ( Rea z2)), (( Im1 z1) + ( Im1 z2)), (( Im2 z1) + ( Im2 z2)), (( Im3 z1) + ( Im3 z2))*];

 reconsider z9 = (z1 + z2) as Quaternion;



 A1: ( Rea z) = (( Rea z1) + ( Rea z2)) by Th16

 .= ( Rea z9) by Lm12;



 A2: ( Im1 z) = (( Im1 z1) + ( Im1 z2)) by Th16

 .= ( Im1 z9) by Lm12;



 A3: ( Im2 z) = (( Im2 z1) + ( Im2 z2)) by Th16

 .= ( Im2 z9) by Lm12;

 ( Im3 z) = (( Im3 z1) + ( Im3 z2)) by Th16

 .= ( Im3 z9) by Lm12;

 hence thesis by A1, A2, A3, Th18;

 end;



 Lm14: for x,y,z be Quaternion st z = (x * y) holds ( Rea z) = ((((( Rea x) * ( Rea y)) - (( Im1 x) * ( Im1 y))) - (( Im2 x) * ( Im2 y))) - (( Im3 x) * ( Im3 y))) & ( Im1 z) = ((((( Rea x) * ( Im1 y)) + (( Im1 x) * ( Rea y))) + (( Im2 x) * ( Im3 y))) - (( Im3 x) * ( Im2 y))) & ( Im2 z) = ((((( Rea x) * ( Im2 y)) + (( Im2 x) * ( Rea y))) + (( Im3 x) * ( Im1 y))) - (( Im1 x) * ( Im3 y))) & ( Im3 z) = ((((( Rea x) * ( Im3 y)) + (( Im3 x) * ( Rea y))) + (( Im1 x) * ( Im2 y))) - (( Im2 x) * ( Im1 y)))

 proof

 let x,y,z be Quaternion such that

 A1: z = (x * y);

 consider x1,x2,x3,x4,y1,y2,y3,y4 be Real such that

 A2: x = [*x1, x2, x3, x4*] and

 A3: y = [*y1, y2, y3, y4*] and

 A4: (x * y) = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)), ((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)), ((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)), ((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] by Def9;



 A5: ( Rea x) = x1 by A2, Th16;



 A6: ( Rea y) = y1 by A3, Th16;



 A7: ( Im1 x) = x2 by A2, Th16;



 A8: ( Im1 y) = y2 by A3, Th16;



 A9: ( Im2 x) = x3 by A2, Th16;



 A10: ( Im2 y) = y3 by A3, Th16;



 A11: ( Im3 x) = x4 by A2, Th16;

 ( Im3 y) = y4 by A3, Th16;

 hence thesis by A1, A4, A5, A6, A7, A8, A9, A10, A11, Th16;

 end;



 Lm15: (((z1 + z2) + z3) + z4) = [*(((( Rea z1) + ( Rea z2)) + ( Rea z3)) + ( Rea z4)), (((( Im1 z1) + ( Im1 z2)) + ( Im1 z3)) + ( Im1 z4)), (((( Im2 z1) + ( Im2 z2)) + ( Im2 z3)) + ( Im2 z4)), (((( Im3 z1) + ( Im3 z2)) + ( Im3 z3)) + ( Im3 z4))*]

 proof

 set z = [*(((( Rea z1) + ( Rea z2)) + ( Rea z3)) + ( Rea z4)), (((( Im1 z1) + ( Im1 z2)) + ( Im1 z3)) + ( Im1 z4)), (((( Im2 z1) + ( Im2 z2)) + ( Im2 z3)) + ( Im2 z4)), (((( Im3 z1) + ( Im3 z2)) + ( Im3 z3)) + ( Im3 z4))*];

 reconsider z9 = (((z1 + z2) + z3) + z4) as Quaternion;



 A1: ( Rea z) = (((( Rea z1) + ( Rea z2)) + ( Rea z3)) + ( Rea z4)) by Th16

 .= ( Rea z9) by Lm11;



 A2: ( Im1 z) = (((( Im1 z1) + ( Im1 z2)) + ( Im1 z3)) + ( Im1 z4)) by Th16

 .= ( Im1 z9) by Lm11;



 A3: ( Im2 z) = (((( Im2 z1) + ( Im2 z2)) + ( Im2 z3)) + ( Im2 z4)) by Th16

 .= ( Im2 z9) by Lm11;

 ( Im3 z) = (((( Im3 z1) + ( Im3 z2)) + ( Im3 z3)) + ( Im3 z4)) by Th16

 .= ( Im3 z9) by Lm11;

 hence thesis by A1, A2, A3, Th18;

 end;



 Lm16: (z1 * z2) = [*((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))), ((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))), ((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2))), ((((( Rea z1) * ( Im3 z2)) + (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2)))*]

 proof

 set z = [*((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))), ((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))), ((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2))), ((((( Rea z1) * ( Im3 z2)) + (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2)))*];

 reconsider z9 = (z1 * z2) as Quaternion;



 A1: ( Rea z) = ((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))) by Th16

 .= ( Rea z9) by Lm14;



 A2: ( Im1 z) = ((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))) by Th16

 .= ( Im1 z9) by Lm14;



 A3: ( Im2 z) = ((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2))) by Th16

 .= ( Im2 z9) by Lm14;

 ( Im3 z) = ((((( Rea z1) * ( Im3 z2)) + (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2))) by Th16

 .= ( Im3 z9) by Lm14;

 hence thesis by A1, A2, A3, Th18;

 end;



 Lm17: ( Rea (z1 * z2)) = ((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))) & ( Im1 (z1 * z2)) = ((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))) & ( Im2 (z1 * z2)) = ((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2))) & ( Im3 (z1 * z2)) = ((((( Rea z1) * ( Im3 z2)) + (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2)))

 proof

 (z1 * z2) = [*((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))), ((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))), ((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2))), ((((( Rea z1) * ( Im3 z2)) + (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2)))*] by Lm16;

 hence thesis by Th16;

 end;

 theorem :: QUATERNI:32

 ( Rea (((z1 + z2) + z3) + z4)) = (((( Rea z1) + ( Rea z2)) + ( Rea z3)) + ( Rea z4)) & ( Im1 (((z1 + z2) + z3) + z4)) = (((( Im1 z1) + ( Im1 z2)) + ( Im1 z3)) + ( Im1 z4)) & ( Im2 (((z1 + z2) + z3) + z4)) = (((( Im2 z1) + ( Im2 z2)) + ( Im2 z3)) + ( Im2 z4)) & ( Im3 (((z1 + z2) + z3) + z4)) = (((( Im3 z1) + ( Im3 z2)) + ( Im3 z3)) + ( Im3 z4))

 proof

 (((z1 + z2) + z3) + z4) = [*(((( Rea z1) + ( Rea z2)) + ( Rea z3)) + ( Rea z4)), (((( Im1 z1) + ( Im1 z2)) + ( Im1 z3)) + ( Im1 z4)), (((( Im2 z1) + ( Im2 z2)) + ( Im2 z3)) + ( Im2 z4)), (((( Im3 z1) + ( Im3 z2)) + ( Im3 z3)) + ( Im3 z4))*] by Lm15;

 hence thesis by Th16;

 end;

 reserve x for Real;



 Lm18: z = x implies ( Rea z) = x & ( Im1 z) = 0 & ( Im2 z) = 0 & ( Im3 z) = 0

 proof

 assume

 A1: z = x;

 reconsider xx = x, zz = 0 as Element of REAL by XREAL_0:def 1;



 A2: x = [*xx, zz*] by ARYTM_0:def 5;

 [*xx, zz*] = [*x, 0 , 0 , 0 *] by Lm3;

 hence thesis by A1, A2, Th16;

 end;

 theorem :: QUATERNI:33

 z1 = x implies ( Rea (z1 * )) = 0 & ( Im1 (z1 * )) = x & ( Im2 (z1 * )) = 0 & ( Im3 (z1 * )) = 0

 proof

 assume

 A1: z1 = x;



 A2: ( Rea (z1 * )) = ((((( Rea z1) * ( Rea )) - (( Im1 z1) * ( Im1 ))) - (( Im2 z1) * ( Im2 ))) - (( Im3 z1) * ( Im3 ))) by Lm17;



 A3: ( Im1 (z1 * )) = ((((( Rea z1) * ( Im1 )) + (( Im1 z1) * ( Rea ))) + (( Im2 z1) * ( Im3 ))) - (( Im3 z1) * ( Im2 ))) by Lm17;



 A4: ( Im2 (z1 * )) = ((((( Rea z1) * ( Im2 )) + (( Im2 z1) * ( Rea ))) + (( Im3 z1) * ( Im1 ))) - (( Im1 z1) * ( Im3 ))) by Lm17;

 ( Im3 (z1 * )) = ((((( Rea z1) * ( Im3 )) + (( Im3 z1) * ( Rea ))) + (( Im1 z1) * ( Im2 ))) - (( Im2 z1) * ( Im1 ))) by Lm17;

 hence thesis by A1, A2, A3, A4, Lm18, Th23;

 end;

 theorem :: QUATERNI:34

 z1 = x implies ( Rea (z1 * <j> )) = 0 & ( Im1 (z1 * <j> )) = 0 & ( Im2 (z1 * <j> )) = x & ( Im3 (z1 * <j> )) = 0

 proof

 assume

 A1: z1 = x;



 A2: ( Rea (z1 * <j> )) = ((((( Rea z1) * ( Rea <j> )) - (( Im1 z1) * ( Im1 <j> ))) - (( Im2 z1) * ( Im2 <j> ))) - (( Im3 z1) * ( Im3 <j> ))) by Lm17;



 A3: ( Im1 (z1 * <j> )) = ((((( Rea z1) * ( Im1 <j> )) + (( Im1 z1) * ( Rea <j> ))) + (( Im2 z1) * ( Im3 <j> ))) - (( Im3 z1) * ( Im2 <j> ))) by Lm17;



 A4: ( Im2 (z1 * <j> )) = ((((( Rea z1) * ( Im2 <j> )) + (( Im2 z1) * ( Rea <j> ))) + (( Im3 z1) * ( Im1 <j> ))) - (( Im1 z1) * ( Im3 <j> ))) by Lm17;

 ( Im3 (z1 * <j> )) = ((((( Rea z1) * ( Im3 <j> )) + (( Im3 z1) * ( Rea <j> ))) + (( Im1 z1) * ( Im2 <j> ))) - (( Im2 z1) * ( Im1 <j> ))) by Lm17;

 hence thesis by A1, A2, A3, A4, Lm18, Th24;

 end;

 theorem :: QUATERNI:35

 z1 = x implies ( Rea (z1 * <k> )) = 0 & ( Im1 (z1 * <k> )) = 0 & ( Im2 (z1 * <k> )) = 0 & ( Im3 (z1 * <k> )) = x

 proof

 assume

 A1: z1 = x;



 A2: ( Rea (z1 * <k> )) = ((((( Rea z1) * ( Rea <k> )) - (( Im1 z1) * ( Im1 <k> ))) - (( Im2 z1) * ( Im2 <k> ))) - (( Im3 z1) * ( Im3 <k> ))) by Lm17;



 A3: ( Im1 (z1 * <k> )) = ((((( Rea z1) * ( Im1 <k> )) + (( Im1 z1) * ( Rea <k> ))) + (( Im2 z1) * ( Im3 <k> ))) - (( Im3 z1) * ( Im2 <k> ))) by Lm17;



 A4: ( Im2 (z1 * <k> )) = ((((( Rea z1) * ( Im2 <k> )) + (( Im2 z1) * ( Rea <k> ))) + (( Im3 z1) * ( Im1 <k> ))) - (( Im1 z1) * ( Im3 <k> ))) by Lm17;

 ( Im3 (z1 * <k> )) = ((((( Rea z1) * ( Im3 <k> )) + (( Im3 z1) * ( Rea <k> ))) + (( Im1 z1) * ( Im2 <k> ))) - (( Im2 z1) * ( Im1 <k> ))) by Lm17;

 hence thesis by A1, A2, A3, A4, Lm18, Th24;

 end;

 definition

 let x be Real, y be Quaternion;

 consider y1,y2,y3,y4 be Real such that

 A1: y = [*y1, y2, y3, y4*] by Th2;

 :: QUATERNI:def18

 func x + y -> Number means

 : Def18: ex y1,y2,y3,y4 be Real st y = [*y1, y2, y3, y4*] & it = [*(x + y1), y2, y3, y4*];

 existence

 proof

 take [*(x + y1), y2, y3, y4*];

 thus thesis by A1;

 end;

 uniqueness

 proof

 let c1,c2 be Number;

 given y1,y2,y3,y4 be Real such that

 A2: y = [*y1, y2, y3, y4*] and

 A3: c1 = [*(x + y1), y2, y3, y4*];

 given y19,y29,y39,y49 be Real such that

 A4: y = [*y19, y29, y39, y49*] and

 A5: c2 = [*(x + y19), y29, y39, y49*];



 A6: y1 = y19 by A2, A4, Th5;



 A7: y2 = y29 by A2, A4, Th5;

 y3 = y39 by A2, A4, Th5;

 hence thesis by A2, A3, A4, A5, A6, A7, Th5;

 end;

 end

 definition

 let x be Real, y be Quaternion;

 :: QUATERNI:def19

 func x - y -> Number equals (x + ( - y));

 coherence ;

 end

 definition

 let x be Real, y be Quaternion;

 consider y1,y2,y3,y4 be Real such that

 A1: y = [*y1, y2, y3, y4*] by Th2;

 :: QUATERNI:def20

 func x * y -> Number means

 : Def20: ex y1,y2,y3,y4 be Real st y = [*y1, y2, y3, y4*] & it = [*(x * y1), (x * y2), (x * y3), (x * y4)*];

 existence

 proof

 take [*(x * y1), (x * y2), (x * y3), (x * y4)*];

 thus thesis by A1;

 end;

 uniqueness

 proof

 let c1,c2 be Number;

 given y1,y2,y3,y4 be Real such that

 A2: y = [*y1, y2, y3, y4*] and

 A3: c1 = [*(x * y1), (x * y2), (x * y3), (x * y4)*];

 given y19,y29,y39,y49 be Real such that

 A4: y = [*y19, y29, y39, y49*] and

 A5: c2 = [*(x * y19), (x * y29), (x * y39), (x * y49)*];



 A6: y1 = y19 by A2, A4, Th5;



 A7: y2 = y29 by A2, A4, Th5;

 y3 = y39 by A2, A4, Th5;

 hence thesis by A2, A3, A4, A5, A6, A7, Th5;

 end;

 end

 registration

 let x be Real, z9 be Quaternion;

 cluster (x + z9) -> quaternion;

 coherence

 proof

 ex y1,y2,y3,y4 be Real st z9 = [*y1, y2, y3, y4*] & (x + z9) = [*(x + y1), y2, y3, y4*] by Def18;

 hence thesis;

 end;

 cluster (x * z9) -> quaternion;

 coherence

 proof

 ex y1,y2,y3,y4 be Real st z9 = [*y1, y2, y3, y4*] & (x * z9) = [*(x * y1), (x * y2), (x * y3), (x * y4)*] by Def20;

 hence (x * z9) in QUATERNION ;

 end;

 cluster (x - z9) -> quaternion;

 coherence ;

 end



 Lm19: for x,y,z,w be Real holds [*x, y, z, w*] = (((x + (y * )) + (z * <j> )) + (w * <k> ))

 proof

 let x,y,z,w be Real;

 = [*zz, jj, zz, zz*] by Lm2, Lm3;



 then

 A1: (y * ) = [*(y * 0 ), (y * 1), (y * 0 ), (y * 0 )*] by Def20

 .= [* 0 , y, 0 , 0 *];



 A2: (z * <j> ) = [*(z * 0 ), (z * 0 ), (z * 1), (y * 0 )*] by Def20

 .= [* 0 , 0 , z, 0 *];



 A3: (w * <k> ) = [*(w * 0 ), (w * 0 ), (w * 0 ), (w * 1)*] by Def20

 .= [* 0 , 0 , 0 , w*];

 (x + (y * )) = [*(x + 0 ), y, 0 , 0 *] by A1, Def18

 .= [*x, y, 0 , 0 *];



 then ((x + (y * )) + (z * <j> )) = [*(x + 0 ), (y + 0 ), ( 0 + z), ( 0 + 0 )*] by A2, Def6

 .= [*x, y, z, 0 *];

 then (((x + (y * )) + (z * <j> )) + (w * <k> )) = [*(x + 0 ), (y + 0 ), ( 0 + z), ( 0 + w)*] by A3, Def6;

 hence thesis;

 end;

 definition

 let z1,z2 be Quaternion;

 :: original: +

 redefine

 func z1 + z2 -> Element of QUATERNION ;

 coherence by Def2;

 end



 Lm20: (z1 + z2) = ((((( Rea z1) + ( Rea z2)) + ((( Im1 z1) + ( Im1 z2)) * )) + ((( Im2 z1) + ( Im2 z2)) * <j> )) + ((( Im3 z1) + ( Im3 z2)) * <k> ))

 proof

 (z1 + z2) = [*(( Rea z1) + ( Rea z2)), (( Im1 z1) + ( Im1 z2)), (( Im2 z1) + ( Im2 z2)), (( Im3 z1) + ( Im3 z2))*] by Lm13;

 hence thesis by Lm19;

 end;

 theorem :: QUATERNI:36



 Th29: ( Rea (z1 + z2)) = (( Rea z1) + ( Rea z2)) & ( Im1 (z1 + z2)) = (( Im1 z1) + ( Im1 z2)) & ( Im2 (z1 + z2)) = (( Im2 z1) + ( Im2 z2)) & ( Im3 (z1 + z2)) = (( Im3 z1) + ( Im3 z2))

 proof

 (z1 + z2) = [*(( Rea z1) + ( Rea z2)), (( Im1 z1) + ( Im1 z2)), (( Im2 z1) + ( Im2 z2)), (( Im3 z1) + ( Im3 z2))*] by Lm13;

 hence thesis by Th16;

 end;

 definition

 let z1,z2 be Quaternion;

 :: original: *

 redefine

 func z1 * z2 -> Element of QUATERNION ;

 coherence by Def2;

 end



 Lm21: (z1 * z2) = (((((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))) + (((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))) * )) + (((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2))) * <j> )) + (((((( Rea z1) * ( Im3 z2)) + (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2))) * <k> ))

 proof

 (z1 * z2) = [*((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))), ((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))), ((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2))), ((((( Rea z1) * ( Im3 z2)) + (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2)))*] by Lm16;

 hence thesis by Lm19;

 end;

 theorem :: QUATERNI:37

 z = (((( Rea z) + (( Im1 z) * )) + (( Im2 z) * <j> )) + (( Im3 z) * <k> ))

 proof

 [*( Rea z), ( Im1 z), ( Im2 z), ( Im3 z)*] = z by Th17;

 hence thesis by Lm19;

 end;



 Lm22: for c be Quaternion holds (c + 0q ) = c

 proof

 let c be Quaternion;



 A1: 0q = [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by ARYTM_0:def 5

 .= [* 0 , 0 , 0 , 0 *] by Lm3;

 consider x,y,w,z be Real such that

 A2: c = [*x, y, w, z*] by Th2;

 (c + 0q ) = [*(x + 0 ), (y + 0 ), (w + 0 ), (z + 0 )*] by A1, A2, Def6

 .= [*x, y, w, z*];

 hence thesis by A2;

 end;



 Lm23: ( 0 * ) = 0 & ( 0 * <j> ) = 0 & ( 0 * <k> ) = 0

 proof

 set z1 = 0 , z2 = ;

 consider y1,y2,y3,y4 be Real such that

 A1: = [*y1, y2, y3, y4*] & (z1 * z2) = [*(z1 * y1), (z1 * y2), (z1 * y3), (z1 * y4)*] by Def20;



 A2: (z1 * z2) = [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by A1, Lm3

 .= 0 by ARYTM_0:def 5;

 consider y1,y2,y3,y4 be Real such that

 A3: <j> = [*y1, y2, y3, y4*] & (z1 * <j> ) = [*(z1 * y1), (z1 * y2), (z1 * y3), (z1 * y4)*] by Def20;



 A4: (z1 * <j> ) = [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by A3, Lm3

 .= 0 by ARYTM_0:def 5;

 consider y1,y2,y3,y4 be Real such that

 A5: <k> = [*y1, y2, y3, y4*] & (z1 * <k> ) = [*(z1 * y1), (z1 * y2), (z1 * y3), (z1 * y4)*] by Def20;

 (z1 * <k> ) = [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by A5, Lm3

 .= 0 by ARYTM_0:def 5;

 hence thesis by A2, A4;

 end;

 theorem :: QUATERNI:38

 ( Im1 z1) = 0 & ( Im1 z2) = 0 & ( Im2 z1) = 0 & ( Im2 z2) = 0 & ( Im3 z1) = 0 & ( Im3 z2) = 0 implies ( Rea (z1 * z2)) = (( Rea z1) * ( Rea z2)) & ( Im1 (z1 * z2)) = ((( Im2 z1) * ( Im3 z2)) - (( Im3 z1) * ( Im2 z2))) & ( Im2 (z1 * z2)) = ((( Im3 z1) * ( Im1 z2)) - (( Im1 z1) * ( Im3 z2))) & ( Im3 (z1 * z2)) = ((( Im1 z1) * ( Im2 z2)) - (( Im2 z1) * ( Im1 z2)))

 proof

 assume

 A1: ( Im1 z1) = 0 & ( Im1 z2) = 0 & ( Im2 z1) = 0 & ( Im2 z2) = 0 & ( Im3 z1) = 0 & ( Im3 z2) = 0 ;



 A2: (z1 * z2) = (((((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))) + (((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))) * )) + (((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2))) * <j> )) + (((((( Rea z1) * ( Im3 z2)) + (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2))) * <k> )) by Lm21

 .= (((( Rea z1) * ( Rea z2)) + 0q ) + 0q ) by Lm22, Lm23, A1

 .= ((( Rea z1) * ( Rea z2)) + 0q ) by Lm22;

 consider y1,y2,y3,y4 be Real such that

 A3: 0q = [*y1, y2, y3, y4*] & ((( Rea z1) * ( Rea z2)) + 0q ) = [*((( Rea z1) * ( Rea z2)) + y1), y2, y3, y4*] by Def18;

 reconsider RR = (( Rea z1) * ( Rea z2)), zz = 0 as Element of REAL by XREAL_0:def 1;

 y1 = 0 & y2 = 0 & y3 = 0 & y4 = 0 by Th5, A3, Lm6;

 then ((( Rea z1) * ( Rea z2)) + 0q ) = [*RR, zz*] by A3, Lm3;

 then ((( Rea z1) * ( Rea z2)) + 0q ) = (( Rea z1) * ( Rea z2)) by ARYTM_0:def 5;

 hence thesis by Lm18, A2, A1;

 end;

 theorem :: QUATERNI:39

 ( Rea z1) = 0 & ( Rea z2) = 0 implies ( Rea (z1 * z2)) = ((( - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))) & ( Im1 (z1 * z2)) = ((( Im2 z1) * ( Im3 z2)) - (( Im3 z1) * ( Im2 z2))) & ( Im2 (z1 * z2)) = ((( Im3 z1) * ( Im1 z2)) - (( Im1 z1) * ( Im3 z2))) & ( Im3 (z1 * z2)) = ((( Im1 z1) * ( Im2 z2)) - (( Im2 z1) * ( Im1 z2)))

 proof

 assume

 A1: ( Rea z1) = 0 & ( Rea z2) = 0 ;

 ( Rea (z1 * z2)) = ((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))) & ( Im1 (z1 * z2)) = ((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))) & ( Im2 (z1 * z2)) = ((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2))) & ( Im3 (z1 * z2)) = ((((( Rea z1) * ( Im3 z2)) + (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2))) by Lm17;

 hence thesis by A1;

 end;

 theorem :: QUATERNI:40

 ( Rea (z * z)) = ((((( Rea z) ^2 ) - (( Im1 z) ^2 )) - (( Im2 z) ^2 )) - (( Im3 z) ^2 )) & ( Im1 (z * z)) = (2 * (( Rea z) * ( Im1 z))) & ( Im2 (z * z)) = (2 * (( Rea z) * ( Im2 z))) & ( Im3 (z * z)) = (2 * (( Rea z) * ( Im3 z)))

 proof

 ( Rea (z * z)) = ((((( Rea z) * ( Rea z)) - (( Im1 z) * ( Im1 z))) - (( Im2 z) * ( Im2 z))) - (( Im3 z) * ( Im3 z))) & ( Im1 (z * z)) = ((((( Rea z) * ( Im1 z)) + (( Im1 z) * ( Rea z))) + (( Im2 z) * ( Im3 z))) - (( Im3 z) * ( Im2 z))) & ( Im2 (z * z)) = ((((( Rea z) * ( Im2 z)) + (( Im2 z) * ( Rea z))) + (( Im3 z) * ( Im1 z))) - (( Im1 z) * ( Im3 z))) & ( Im3 (z * z)) = ((((( Rea z) * ( Im3 z)) + (( Im3 z) * ( Rea z))) + (( Im1 z) * ( Im2 z))) - (( Im2 z) * ( Im1 z))) by Lm17;

 hence thesis;

 end;

 definition

 let z be Quaternion;

 :: original: -

 redefine

 func - z -> Element of QUATERNION ;

 coherence by Def2;

 end



 Lm24: ( - z) = (((( - ( Rea z)) + (( - ( Im1 z)) * )) + (( - ( Im2 z)) * <j> )) + (( - ( Im3 z)) * <k> ))

 proof

 set z9 = [*( - ( Rea z)), ( - ( Im1 z)), ( - ( Im2 z)), ( - ( Im3 z))*];



 A1: z9 = (((( - ( Rea z)) + (( - ( Im1 z)) * )) + (( - ( Im2 z)) * <j> )) + (( - ( Im3 z)) * <k> )) by Lm19;

 (z9 + z) = [*(( Rea z9) + ( Rea z)), (( Im1 z9) + ( Im1 z)), (( Im2 z9) + ( Im2 z)), (( Im3 z9) + ( Im3 z))*] by Lm13

 .= [*(( - ( Rea z)) + ( Rea z)), (( Im1 z9) + ( Im1 z)), (( Im2 z9) + ( Im2 z)), (( Im3 z9) + ( Im3 z))*] by Th16

 .= [* 0 , (( - ( Im1 z)) + ( Im1 z)), (( Im2 z9) + ( Im2 z)), (( Im3 z9) + ( Im3 z))*] by Th16

 .= [* 0 , 0 , (( - ( Im2 z)) + ( Im2 z)), (( Im3 z9) + ( Im3 z))*] by Th16

 .= [* 0 , 0 , 0 , (( - ( Im3 z)) + ( Im3 z))*] by Th16

 .= 0 by Lm6;

 hence thesis by A1, Def7;

 end;

 theorem :: QUATERNI:41



 Th34: ( Rea ( - z)) = ( - ( Rea z)) & ( Im1 ( - z)) = ( - ( Im1 z)) & ( Im2 ( - z)) = ( - ( Im2 z)) & ( Im3 ( - z)) = ( - ( Im3 z))

 proof

 ( - z) = (((( - ( Rea z)) + (( - ( Im1 z)) * )) + (( - ( Im2 z)) * <j> )) + (( - ( Im3 z)) * <k> )) by Lm24;

 then ( - z) = [*( - ( Rea z)), ( - ( Im1 z)), ( - ( Im2 z)), ( - ( Im3 z))*] by Lm19;

 hence thesis by Th16;

 end;

 definition

 let z1,z2 be Quaternion;

 :: original: -

 redefine

 func z1 - z2 -> Element of QUATERNION ;

 coherence by Def2;

 end



 Lm25: (z1 - z2) = ((((( Rea z1) - ( Rea z2)) + ((( Im1 z1) - ( Im1 z2)) * )) + ((( Im2 z1) - ( Im2 z2)) * <j> )) + ((( Im3 z1) - ( Im3 z2)) * <k> ))

 proof

 (z1 - z2) = ((((( Rea z1) + ( Rea ( - z2))) + ((( Im1 z1) + ( Im1 ( - z2))) * )) + ((( Im2 z1) + ( Im2 ( - z2))) * <j> )) + ((( Im3 z1) + ( Im3 ( - z2))) * <k> )) by Lm20

 .= ((((( Rea z1) + ( - ( Rea z2))) + ((( Im1 z1) + ( Im1 ( - z2))) * )) + ((( Im2 z1) + ( Im2 ( - z2))) * <j> )) + ((( Im3 z1) + ( Im3 ( - z2))) * <k> )) by Th34

 .= ((((( Rea z1) + ( - ( Rea z2))) + ((( Im1 z1) - ( Im1 z2)) * )) + ((( Im2 z1) + ( Im2 ( - z2))) * <j> )) + ((( Im3 z1) + ( Im3 ( - z2))) * <k> )) by Th34

 .= ((((( Rea z1) + ( - ( Rea z2))) + ((( Im1 z1) - ( Im1 z2)) * )) + ((( Im2 z1) + ( - ( Im2 z2))) * <j> )) + ((( Im3 z1) + ( Im3 ( - z2))) * <k> )) by Th34

 .= ((((( Rea z1) - ( Rea z2)) + ((( Im1 z1) - ( Im1 z2)) * )) + ((( Im2 z1) - ( Im2 z2)) * <j> )) + ((( Im3 z1) - ( Im3 z2)) * <k> )) by Th34;

 hence thesis;

 end;

 theorem :: QUATERNI:42



 Th35: ( Rea (z1 - z2)) = (( Rea z1) - ( Rea z2)) & ( Im1 (z1 - z2)) = (( Im1 z1) - ( Im1 z2)) & ( Im2 (z1 - z2)) = (( Im2 z1) - ( Im2 z2)) & ( Im3 (z1 - z2)) = (( Im3 z1) - ( Im3 z2))

 proof

 (z1 - z2) = ((((( Rea z1) - ( Rea z2)) + ((( Im1 z1) - ( Im1 z2)) * )) + ((( Im2 z1) - ( Im2 z2)) * <j> )) + ((( Im3 z1) - ( Im3 z2)) * <k> )) by Lm25;

 then (z1 - z2) = [*(( Rea z1) - ( Rea z2)), (( Im1 z1) - ( Im1 z2)), (( Im2 z1) - ( Im2 z2)), (( Im3 z1) - ( Im3 z2))*] by Lm19;

 hence thesis by Th16;

 end;

 definition

 let z be Quaternion;

 :: QUATERNI:def21

 func z *' -> Quaternion equals (((( Rea z) + (( - ( Im1 z)) * )) + (( - ( Im2 z)) * <j> )) + (( - ( Im3 z)) * <k> ));

 coherence ;

 end

 definition

 let z be Quaternion;

 :: original: *'

 redefine

 func z *' -> Element of QUATERNION ;

 coherence ;

 end

 theorem :: QUATERNI:43



 Th36: (z *' ) = [*( Rea z), ( - ( Im1 z)), ( - ( Im2 z)), ( - ( Im3 z))*]

 proof

 = [*zz, jj, zz, zz*] by Lm2, Lm3;



 then (z *' ) = (((( Rea z) + [*(( - ( Im1 z)) * 0 ), (( - ( Im1 z)) * 1), (( - ( Im1 z)) * 0 ), (( - ( Im1 z)) * 0 )*]) + (( - ( Im2 z)) * <j> )) + (( - ( Im3 z)) * <k> )) by Def20

 .= (((( Rea z) + [* 0 , ( - ( Im1 z)), 0 , 0 *]) + [*(( - ( Im2 z)) * 0 ), (( - ( Im2 z)) * 0 ), (( - ( Im2 z)) * 1), (( - ( Im2 z)) * 0 )*]) + (( - ( Im3 z)) * <k> )) by Def20

 .= (((( Rea z) + [* 0 , ( - ( Im1 z)), 0 , 0 *]) + [* 0 , 0 , ( - ( Im2 z)), 0 *]) + [*(( - ( Im3 z)) * 0 ), (( - ( Im3 z)) * 0 ), (( - ( Im3 z)) * 0 ), (( - ( Im3 z)) * 1)*]) by Def20

 .= (( [*(( Rea z) + 0 ), ( - ( Im1 z)), 0 , 0 *] + [* 0 , 0 , ( - ( Im2 z)), 0 *]) + [* 0 , 0 , 0 , ( - ( Im3 z))*]) by Def18

 .= ( [*(( Rea z) + 0 ), (( - ( Im1 z)) + 0 ), ( 0 + ( - ( Im2 z))), ( 0 + 0 )*] + [* 0 , 0 , 0 , ( - ( Im3 z))*]) by Def6

 .= [*(( Rea z) + 0 ), (( - ( Im1 z)) + 0 ), (( - ( Im2 z)) + 0 ), ( 0 + ( - ( Im3 z)))*] by Def6;

 hence thesis;

 end;

 theorem :: QUATERNI:44

 ( Rea (z *' )) = ( Rea z) & ( Im1 (z *' )) = ( - ( Im1 z)) & ( Im2 (z *' )) = ( - ( Im2 z)) & ( Im3 (z *' )) = ( - ( Im3 z))

 proof

 (z *' ) = [*( Rea z), ( - ( Im1 z)), ( - ( Im2 z)), ( - ( Im3 z))*] by Lm19;

 hence thesis by Th16;

 end;

 theorem :: QUATERNI:45

 z = 0 implies (z *' ) = 0

 proof

 assume

 A1: z = 0 ;

 then

 A2: ( Rea z) = 0 by Lm6, Th16;



 A3: ( Im1 z) = 0 by A1, Lm6, Th16;



 A4: ( Im2 z) = 0 by A1, Lm6, Th16;

 ( Im3 z) = 0 by A1, Lm6, Th16;

 hence thesis by A2, A3, A4, Lm6, Th36;

 end;

 theorem :: QUATERNI:46

 (z *' ) = 0 implies z = 0

 proof

 assume

 A1: (z *' ) = 0 ;



 A2: (z *' ) = [*( Rea z), ( - ( Im1 z)), ( - ( Im2 z)), ( - ( Im3 z))*] by Th36;



 A3: ( Rea (z *' )) = 0 by A1, Lm6, Th16;



 A4: ( Im1 (z *' )) = 0 by A1, Lm6, Th16;



 A5: ( Im2 (z *' )) = 0 by A1, Lm6, Th16;



 A6: ( Im3 (z *' )) = 0 by A1, Lm6, Th16;



 A7: ( Rea (z *' )) = ( Rea z) by A2, Th16;



 A8: ( Im1 (z *' )) = ( - ( Im1 z)) by A2, Th16;



 A9: ( Im2 (z *' )) = ( - ( Im2 z)) by A2, Th16;

 ( Im3 (z *' )) = ( - ( Im3 z)) by A2, Th16;

 hence thesis by A3, A4, A5, A6, A7, A8, A9, Th19;

 end;

 theorem :: QUATERNI:47

 ( 1q *' ) = 1q

 proof

 [*jj, zz*] = [*1, 0 , 0 , 0 *] by Lm3;

 then

 A1: 1q = [*1, 0 , 0 , 0 *] by ARYTM_0:def 5;



 A2: ( Rea [*jj, zz, zz, zz*]) = 1 by Th16;



 A3: ( Im1 [*jj, zz, zz, zz*]) = 0 by Th16;



 A4: ( Im2 [*jj, zz, zz, zz*]) = 0 by Th16;

 ( Im3 [*jj, zz, zz, zz*]) = 0 by Th16;

 hence thesis by A1, A2, A3, A4, Th36;

 end;

 theorem :: QUATERNI:48

 ( Rea ( *' )) = 0 & ( Im1 ( *' )) = ( - 1) & ( Im2 ( *' )) = 0 & ( Im3 ( *' )) = 0

 proof

 ( *' ) = [*zz, ( - jj), zz, zz*] by Th23, Th36;

 hence thesis by Th16;

 end;

 theorem :: QUATERNI:49

 ( Rea ( <j> *' )) = 0 & ( Im1 ( <j> *' )) = 0 & ( Im2 ( <j> *' )) = ( - 1) & ( Im3 ( <j> *' )) = 0

 proof

 ( <j> *' ) = [*zz, zz, ( - jj), zz*] by Th24, Th36;

 hence thesis by Th16;

 end;

 theorem :: QUATERNI:50

 ( Rea ( <k> *' )) = 0 & ( Im1 ( <k> *' )) = 0 & ( Im2 ( <k> *' )) = 0 & ( Im3 ( <k> *' )) = ( - 1)

 proof

 ( <k> *' ) = [*zz, zz, zz, ( - jj)*] by Th24, Th36;

 hence thesis by Th16;

 end;

 theorem :: QUATERNI:51

 ( *' ) = ( - ) by Th23, Lm24;

 theorem :: QUATERNI:52

 ( <j> *' ) = ( - <j> ) by Th24, Lm24;

 theorem :: QUATERNI:53

 ( <k> *' ) = ( - <k> ) by Th24, Lm24;

 theorem :: QUATERNI:54

 ((z1 + z2) *' ) = ((z1 *' ) + (z2 *' ))

 proof



 A1: (z1 *' ) = [*( Rea z1), ( - ( Im1 z1)), ( - ( Im2 z1)), ( - ( Im3 z1))*] by Th36;



 A2: (z2 *' ) = [*( Rea z2), ( - ( Im1 z2)), ( - ( Im2 z2)), ( - ( Im3 z2))*] by Th36;



 A3: ((z1 + z2) *' ) = [*( Rea (z1 + z2)), ( - ( Im1 (z1 + z2))), ( - ( Im2 (z1 + z2))), ( - ( Im3 (z1 + z2)))*] by Th36;

 ((z1 *' ) + (z2 *' )) = [*(( Rea z1) + ( Rea z2)), (( - ( Im1 z1)) + ( - ( Im1 z2))), (( - ( Im2 z1)) + ( - ( Im2 z2))), (( - ( Im3 z1)) + ( - ( Im3 z2)))*] by A1, A2, Def6

 .= [*( Rea (z1 + z2)), ( - (( Im1 z1) + ( Im1 z2))), ( - (( Im2 z1) + ( Im2 z2))), ( - (( Im3 z1) + ( Im3 z2)))*] by Th29

 .= [*( Rea (z1 + z2)), ( - ( Im1 (z1 + z2))), ( - (( Im2 z1) + ( Im2 z2))), ( - (( Im3 z1) + ( Im3 z2)))*] by Th29

 .= [*( Rea (z1 + z2)), ( - ( Im1 (z1 + z2))), ( - ( Im2 (z1 + z2))), ( - (( Im3 z1) + ( Im3 z2)))*] by Th29;

 hence thesis by A3, Th29;

 end;

 theorem :: QUATERNI:55



 Th48: (( - z) *' ) = ( - (z *' ))

 proof



 A1: (z *' ) = [*( Rea z), ( - ( Im1 z)), ( - ( Im2 z)), ( - ( Im3 z))*] by Th36;

 (( - z) *' ) = [*( Rea ( - z)), ( - ( Im1 ( - z))), ( - ( Im2 ( - z))), ( - ( Im3 ( - z)))*] by Th36;



 then (( - z) *' ) = [*( - ( Rea z)), ( - ( Im1 ( - z))), ( - ( Im2 ( - z))), ( - ( Im3 ( - z)))*] by Th34

 .= [*( - ( Rea z)), ( - ( - ( Im1 z))), ( - ( Im2 ( - z))), ( - ( Im3 ( - z)))*] by Th34

 .= [*( - ( Rea z)), ( Im1 z), ( - ( - ( Im2 z))), ( - ( Im3 ( - z)))*] by Th34

 .= [*( - ( Rea z)), ( Im1 z), ( Im2 z), ( - ( - ( Im3 z)))*] by Th34

 .= [*( - ( Rea z)), ( Im1 z), ( Im2 z), ( Im3 z)*];



 then ((z *' ) + (( - z) *' )) = [*(( Rea z) + ( - ( Rea z))), (( - ( Im1 z)) + ( Im1 z)), (( - ( Im2 z)) + ( Im2 z)), (( - ( Im3 z)) + ( Im3 z))*] by A1, Def6

 .= 0 by Lm6;

 hence thesis by Def7;

 end;

 theorem :: QUATERNI:56

 ((z1 - z2) *' ) = ((z1 *' ) - (z2 *' ))

 proof



 A1: (z1 *' ) = [*( Rea z1), ( - ( Im1 z1)), ( - ( Im2 z1)), ( - ( Im3 z1))*] by Th36;



 A2: (( - z2) *' ) = [*( Rea ( - z2)), ( - ( Im1 ( - z2))), ( - ( Im2 ( - z2))), ( - ( Im3 ( - z2)))*] by Th36;



 A3: ((z1 - z2) *' ) = [*( Rea (z1 - z2)), ( - ( Im1 (z1 - z2))), ( - ( Im2 (z1 - z2))), ( - ( Im3 (z1 - z2)))*] by Th36;



 A4: ((z1 *' ) - (z2 *' )) = ((z1 *' ) + (( - z2) *' )) by Th48

 .= [*(( Rea z1) + ( Rea ( - z2))), (( - ( Im1 z1)) + ( - ( Im1 ( - z2)))), (( - ( Im2 z1)) + ( - ( Im2 ( - z2)))), (( - ( Im3 z1)) + ( - ( Im3 ( - z2))))*] by A1, A2, Def6

 .= [*(( Rea z1) + ( - ( Rea z2))), (( - ( Im1 z1)) + ( - ( Im1 ( - z2)))), (( - ( Im2 z1)) + ( - ( Im2 ( - z2)))), (( - ( Im3 z1)) + ( - ( Im3 ( - z2))))*] by Th34

 .= [*(( Rea z1) - ( Rea z2)), (( - ( Im1 z1)) - ( - ( Im1 z2))), (( - ( Im2 z1)) + ( - ( Im2 ( - z2)))), (( - ( Im3 z1)) + ( - ( Im3 ( - z2))))*] by Th34

 .= [*(( Rea z1) - ( Rea z2)), (( - ( Im1 z1)) + ( Im1 z2)), (( - ( Im2 z1)) - ( - ( Im2 z2))), (( - ( Im3 z1)) + ( - ( Im3 ( - z2))))*] by Th34

 .= [*(( Rea z1) - ( Rea z2)), (( - ( Im1 z1)) + ( Im1 z2)), (( - ( Im2 z1)) + ( Im2 z2)), (( - ( Im3 z1)) - ( - ( Im3 z2)))*] by Th34

 .= [*(( Rea z1) - ( Rea z2)), (( - ( Im1 z1)) + ( Im1 z2)), (( - ( Im2 z1)) + ( Im2 z2)), (( - ( Im3 z1)) + ( Im3 z2))*];

 ((z1 - z2) *' ) = [*(( Rea z1) - ( Rea z2)), ( - ( Im1 (z1 - z2))), ( - ( Im2 (z1 - z2))), ( - ( Im3 (z1 - z2)))*] by A3, Th35

 .= [*(( Rea z1) - ( Rea z2)), ( - (( Im1 z1) - ( Im1 z2))), ( - ( Im2 (z1 - z2))), ( - ( Im3 (z1 - z2)))*] by Th35

 .= [*(( Rea z1) - ( Rea z2)), (( - ( Im1 z1)) + ( Im1 z2)), ( - (( Im2 z1) - ( Im2 z2))), ( - ( Im3 (z1 - z2)))*] by Th35

 .= [*(( Rea z1) - ( Rea z2)), (( - ( Im1 z1)) + ( Im1 z2)), (( - ( Im2 z1)) + ( Im2 z2)), ( - (( Im3 z1) - ( Im3 z2)))*] by Th35;

 hence thesis by A4;

 end;

 theorem :: QUATERNI:57

 ((z1 * z2) *' ) = ((z1 *' ) * (z2 *' )) implies (( Im2 z1) * ( Im3 z2)) = (( Im3 z1) * ( Im2 z2))

 proof

 assume

 A1: ((z1 * z2) *' ) = ((z1 *' ) * (z2 *' ));



 A2: (z1 *' ) = [*( Rea z1), ( - ( Im1 z1)), ( - ( Im2 z1)), ( - ( Im3 z1))*] by Th36;



 A3: (z2 *' ) = [*( Rea z2), ( - ( Im1 z2)), ( - ( Im2 z2)), ( - ( Im3 z2))*] by Th36;



 A4: ((z1 * z2) *' ) = [*( Rea (z1 * z2)), ( - ( Im1 (z1 * z2))), ( - ( Im2 (z1 * z2))), ( - ( Im3 (z1 * z2)))*] by Th36;



 A5: ((z1 *' ) * (z2 *' )) = [*((((( Rea z1) * ( Rea z2)) - (( - ( Im1 z1)) * ( - ( Im1 z2)))) - (( - ( Im2 z1)) * ( - ( Im2 z2)))) - (( - ( Im3 z1)) * ( - ( Im3 z2)))), ((((( Rea z1) * ( - ( Im1 z2))) + (( - ( Im1 z1)) * ( Rea z2))) + (( - ( Im2 z1)) * ( - ( Im3 z2)))) - (( - ( Im3 z1)) * ( - ( Im2 z2)))), ((((( Rea z1) * ( - ( Im2 z2))) + (( Rea z2) * ( - ( Im2 z1)))) + (( - ( Im1 z2)) * ( - ( Im3 z1)))) - (( - ( Im3 z2)) * ( - ( Im1 z1)))), ((((( Rea z1) * ( - ( Im3 z2))) + (( - ( Im3 z1)) * ( Rea z2))) + (( - ( Im1 z1)) * ( - ( Im2 z2)))) - (( - ( Im2 z1)) * ( - ( Im1 z2))))*] by A2, A3, Def9

 .= [*((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))), (((( - (( Rea z1) * ( Im1 z2))) - (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))), (((( - (( Rea z1) * ( Im2 z2))) - (( Rea z2) * ( Im2 z1))) + (( Im1 z2) * ( Im3 z1))) - (( Im3 z2) * ( Im1 z1))), (((( - (( Rea z1) * ( Im3 z2))) - (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2)))*];



 A6: ((z1 * z2) *' ) = [*((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))), ( - ( Im1 (z1 * z2))), ( - ( Im2 (z1 * z2))), ( - ( Im3 (z1 * z2)))*] by A4, Lm17

 .= [*((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))), ( - ((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2)))), ( - ( Im2 (z1 * z2))), ( - ( Im3 (z1 * z2)))*] by Lm17

 .= [*((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))), ( - ((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2)))), ( - ((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2)))), ( - ( Im3 (z1 * z2)))*] by Lm17

 .= [*((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))), ( - ((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2)))), ( - ((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2)))), ( - ((((( Rea z1) * ( Im3 z2)) + (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2))))*] by Lm17

 .= [*((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))), (((( - (( Rea z1) * ( Im1 z2))) - (( Im1 z1) * ( Rea z2))) - (( Im2 z1) * ( Im3 z2))) + (( Im3 z1) * ( Im2 z2))), (((( - (( Rea z1) * ( Im2 z2))) - (( Im2 z1) * ( Rea z2))) - (( Im3 z1) * ( Im1 z2))) + (( Im1 z1) * ( Im3 z2))), (((( - (( Rea z1) * ( Im3 z2))) - (( Im3 z1) * ( Rea z2))) - (( Im1 z1) * ( Im2 z2))) + (( Im2 z1) * ( Im1 z2)))*];



 A7: ( Im1 ((z1 *' ) * (z2 *' ))) = (((( - (( Rea z1) * ( Im1 z2))) - (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))) by A5, Th16;

 ( Im1 ((z1 * z2) *' )) = (((( - (( Rea z1) * ( Im1 z2))) - (( Im1 z1) * ( Rea z2))) - (( Im2 z1) * ( Im3 z2))) + (( Im3 z1) * ( Im2 z2))) by A6, Th16;

 hence thesis by A1, A7;

 end;

 theorem :: QUATERNI:58

 ( Im1 z) = 0 & ( Im2 z) = 0 & ( Im3 z) = 0 implies (z *' ) = z

 proof

 assume that

 A1: ( Im1 z) = 0 and

 A2: ( Im2 z) = 0 and

 A3: ( Im3 z) = 0 ;

 reconsider Rz = ( Rea z), zz = 0 as Element of REAL by XREAL_0:def 1;



 A4: z = [*( Rea z), 0 , 0 , 0 *] by A1, A2, A3, Th17

 .= [*Rz, zz*] by Lm3

 .= ( Rea z) by ARYTM_0:def 5;

 (z *' ) = [*( Rea z), 0 , 0 , 0 *] by A1, A2, A3, Th36

 .= [*Rz, zz*] by Lm3

 .= ( Rea z) by ARYTM_0:def 5;

 hence thesis by A4;

 end;

 theorem :: QUATERNI:59

 ( Rea z) = 0 implies (z *' ) = ( - z)

 proof

 assume

 A1: ( Rea z) = 0 ;

 ( - z) = (((( - ( Rea z)) + (( - ( Im1 z)) * )) + (( - ( Im2 z)) * <j> )) + (( - ( Im3 z)) * <k> )) by Lm24;

 hence thesis by A1;

 end;

 theorem :: QUATERNI:60

 ( Rea (z * (z *' ))) = ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )) & ( Im1 (z * (z *' ))) = 0 & ( Im2 (z * (z *' ))) = 0 & ( Im3 (z * (z *' ))) = 0

 proof



 A1: z = [*( Rea z), ( Im1 z), ( Im2 z), ( Im3 z)*] by Th17;

 (z *' ) = [*( Rea z), ( - ( Im1 z)), ( - ( Im2 z)), ( - ( Im3 z))*] by Th36;



 then (z * (z *' )) = [*((((( Rea z) * ( Rea z)) - (( Im1 z) * ( - ( Im1 z)))) - (( Im2 z) * ( - ( Im2 z)))) - (( Im3 z) * ( - ( Im3 z)))), ((((( Rea z) * ( - ( Im1 z))) + (( Im1 z) * ( Rea z))) + (( Im2 z) * ( - ( Im3 z)))) - (( Im3 z) * ( - ( Im2 z)))), ((((( Rea z) * ( - ( Im2 z))) + (( Rea z) * ( Im2 z))) + (( - ( Im1 z)) * ( Im3 z))) - (( - ( Im3 z)) * ( Im1 z))), ((((( Rea z) * ( - ( Im3 z))) + (( Im3 z) * ( Rea z))) + (( Im1 z) * ( - ( Im2 z)))) - (( Im2 z) * ( - ( Im1 z))))*] by A1, Def9

 .= [*((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )), 0 , 0 , 0 *];

 hence thesis by Th16;

 end;

 theorem :: QUATERNI:61

 ( Rea (z + (z *' ))) = (2 * ( Rea z)) & ( Im1 (z + (z *' ))) = 0 & ( Im2 (z + (z *' ))) = 0 & ( Im3 (z + (z *' ))) = 0

 proof



 A1: z = [*( Rea z), ( Im1 z), ( Im2 z), ( Im3 z)*] by Th17;

 (z *' ) = [*( Rea z), ( - ( Im1 z)), ( - ( Im2 z)), ( - ( Im3 z))*] by Th36;



 then (z + (z *' )) = [*(( Rea z) + ( Rea z)), (( Im1 z) + ( - ( Im1 z))), (( Im2 z) + ( - ( Im2 z))), (( Im3 z) + ( - ( Im3 z)))*] by A1, Def6

 .= [*(2 * ( Rea z)), 0 , 0 , 0 *];

 hence thesis by Th16;

 end;

 theorem :: QUATERNI:62



 Th55: ( - z) = [*( - ( Rea z)), ( - ( Im1 z)), ( - ( Im2 z)), ( - ( Im3 z))*]

 proof



 A1: z = [*( Rea z), ( Im1 z), ( Im2 z), ( Im3 z)*] by Th17;

 set z9 = [*( - ( Rea z)), ( - ( Im1 z)), ( - ( Im2 z)), ( - ( Im3 z))*];

 (z + z9) = [*(( Rea z) + ( - ( Rea z))), (( Im1 z) + ( - ( Im1 z))), (( Im2 z) + ( - ( Im2 z))), (( Im3 z) + ( - ( Im3 z)))*] by A1, Def6

 .= 0 by Lm6;

 hence thesis by Def7;

 end;

 theorem :: QUATERNI:63

 (z1 - z2) = [*(( Rea z1) - ( Rea z2)), (( Im1 z1) - ( Im1 z2)), (( Im2 z1) - ( Im2 z2)), (( Im3 z1) - ( Im3 z2))*]

 proof



 A1: z1 = [*( Rea z1), ( Im1 z1), ( Im2 z1), ( Im3 z1)*] by Th17;



 A2: z2 = [*( Rea z2), ( Im1 z2), ( Im2 z2), ( Im3 z2)*] by Th17;

 set z9 = [*( - ( Rea z2)), ( - ( Im1 z2)), ( - ( Im2 z2)), ( - ( Im3 z2))*];

 (z2 + z9) = [*(( Rea z2) + ( - ( Rea z2))), (( Im1 z2) + ( - ( Im1 z2))), (( Im2 z2) + ( - ( Im2 z2))), (( Im3 z2) + ( - ( Im3 z2)))*] by A2, Def6

 .= 0 by Lm6;

 then ( - z2) = [*( - ( Rea z2)), ( - ( Im1 z2)), ( - ( Im2 z2)), ( - ( Im3 z2))*] by Def7;

 hence thesis by A1, Def6;

 end;

 theorem :: QUATERNI:64

 ( Rea (z - (z *' ))) = 0 & ( Im1 (z - (z *' ))) = (2 * ( Im1 z)) & ( Im2 (z - (z *' ))) = (2 * ( Im2 z)) & ( Im3 (z - (z *' ))) = (2 * ( Im3 z))

 proof



 A1: z = [*( Rea z), ( Im1 z), ( Im2 z), ( Im3 z)*] by Th17;



 A2: (z *' ) = [*( Rea z), ( - ( Im1 z)), ( - ( Im2 z)), ( - ( Im3 z))*] by Th36;



 A3: ( Im1 (z *' )) = ( - ( Im1 z)) by A2, Th16;



 A4: ( Im2 (z *' )) = ( - ( Im2 z)) by A2, Th16;



 A5: ( Im3 (z *' )) = ( - ( Im3 z)) by A2, Th16;

 set zz = (z *' );

 ( - zz) = [*( - ( Rea zz)), ( - ( Im1 zz)), ( - ( Im2 zz)), ( - ( Im3 zz))*] by Th55;

 then ( - zz) = [*( - ( Rea z)), ( Im1 z), ( Im2 z), ( Im3 z)*] by A2, Th16, A3, A4, A5;



 then (z - zz) = [*(( Rea z) + ( - ( Rea z))), (( Im1 z) + ( Im1 z)), (( Im2 z) + ( Im2 z)), (( Im3 z) + ( Im3 z))*] by A1, Def6

 .= [* 0 , (2 * ( Im1 z)), (2 * ( Im2 z)), (2 * ( Im3 z))*];

 hence thesis by Th16;

 end;

 definition

 let z;

 :: QUATERNI:def22

 func |.z.| -> Real equals ( sqrt ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )));

 coherence ;

 end

 theorem :: QUATERNI:65



 Th58: |. 0q .| = 0

 proof



 A1: ( Rea 0q ) = 0 by Lm6, Th16;



 A2: ( Im1 0q ) = 0 by Lm6, Th16;

 ( Im2 0q ) = 0 by Lm6, Th16;

 hence thesis by A1, A2, Lm6, Th16, SQUARE_1: 17;

 end;

 theorem :: QUATERNI:66



 Th59: |.z.| = 0 implies z = 0

 proof

 assume

 A1: |.z.| = 0 ;



 A2: 0 <= (( Rea z) ^2 ) by XREAL_1: 63;



 A3: 0 <= (( Im1 z) ^2 ) by XREAL_1: 63;



 A4: 0 <= (( Im2 z) ^2 ) by XREAL_1: 63;

 0 <= (( Im3 z) ^2 ) by XREAL_1: 63;

 then

 A5: 0 = ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )) by A1, A2, A3, A4, SQUARE_1: 25;

 then

 A6: ( Rea z) = 0 by Lm9;



 A7: ( Im1 z) = 0 by A5, Lm9;



 A8: ( Im2 z) = 0 by A5, Lm9;

 ( Im3 z) = 0 by A5, Lm9;

 hence thesis by A6, A7, A8, Lm6, Th17;

 end;

 theorem :: QUATERNI:67



 Th60: 0 <= |.z.|

 proof



 A1: 0 <= (( Rea z) ^2 ) by XREAL_1: 63;



 A2: 0 <= (( Im1 z) ^2 ) by XREAL_1: 63;



 A3: 0 <= (( Im2 z) ^2 ) by XREAL_1: 63;

 0 <= (( Im3 z) ^2 ) by XREAL_1: 63;

 hence thesis by A1, A2, A3, SQUARE_1:def 2;

 end;

 theorem :: QUATERNI:68

 |. 1q .| = 1

 proof



 A1: ( Rea 1q ) = jj by Lm10, Th16;



 A2: ( Im1 1q ) = zz by Lm10, Th16;

 ( Im2 1q ) = zz by Lm10, Th16;

 hence thesis by A1, A2, Lm10, Th16, SQUARE_1: 18;

 end;

 theorem :: QUATERNI:69

 |. .| = 1 by Th23, SQUARE_1: 18;

 theorem :: QUATERNI:70

 |. <j> .| = 1 by Th24, SQUARE_1: 18;

 theorem :: QUATERNI:71

 |. <k> .| = 1 by Th24, SQUARE_1: 18;

 theorem :: QUATERNI:72



 Th65: |.( - z).| = |.z.|

 proof



 A1: ( - z) = [*( - ( Rea z)), ( - ( Im1 z)), ( - ( Im2 z)), ( - ( Im3 z))*] by Th55;

 then

 A2: ( Rea ( - z)) = ( - ( Rea z)) by Th16;



 A3: ( Im1 ( - z)) = ( - ( Im1 z)) by A1, Th16;



 A4: ( Im2 ( - z)) = ( - ( Im2 z)) by A1, Th16;

 ( Im3 ( - z)) = ( - ( Im3 z)) by A1, Th16;

 hence thesis by A2, A3, A4;

 end;

 theorem :: QUATERNI:73



 Th66: |.(z *' ).| = |.z.|

 proof



 A1: (z *' ) = [*( Rea z), ( - ( Im1 z)), ( - ( Im2 z)), ( - ( Im3 z))*] by Th36;

 then

 A2: ( Im1 (z *' )) = ( - ( Im1 z)) by Th16;



 A3: ( Im2 (z *' )) = ( - ( Im2 z)) by A1, Th16;

 ( Im3 (z *' )) = ( - ( Im3 z)) by A1, Th16;

 hence thesis by A1, A2, A3, Th16;

 end;

 theorem :: QUATERNI:74



 Th67: for a,b,c,d be Real holds ((((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 )) >= 0

 proof

 let a,b,c,d be Real;



 A1: (a ^2 ) >= 0 by XREAL_1: 63;



 A2: (b ^2 ) >= 0 by XREAL_1: 63;



 A3: (c ^2 ) >= 0 by XREAL_1: 63;

 (d ^2 ) >= 0 by XREAL_1: 63;

 hence thesis by A1, A2, A3;

 end;



 Lm26: (a ^2 ) <= ((((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 ))

 proof



 A1: 0 <= (c ^2 ) by XREAL_1: 63;



 A2: 0 <= (d ^2 ) by XREAL_1: 63;

 (a ^2 ) <= ((a ^2 ) + (b ^2 )) by XREAL_1: 31, XREAL_1: 63;

 then ( 0 + (a ^2 )) <= (((a ^2 ) + (b ^2 )) + (c ^2 )) by A1, XREAL_1: 7;

 hence thesis by A2, XREAL_1: 7;

 end;



 Lm27: for a,b,c,d be Real holds (c ^2 ) <= ((((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 ))

 proof

 let a,b,c,d be Real;



 A1: 0 <= (b ^2 ) by XREAL_1: 63;



 A2: 0 <= (d ^2 ) by XREAL_1: 63;

 (c ^2 ) <= ((a ^2 ) + (c ^2 )) by XREAL_1: 31, XREAL_1: 63;

 then ( 0 + (c ^2 )) <= (((a ^2 ) + (c ^2 )) + (b ^2 )) by A1, XREAL_1: 7;

 hence thesis by A2, XREAL_1: 7;

 end;



 Lm28: (d ^2 ) <= ((((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 ))

 proof



 A1: 0 <= (b ^2 ) by XREAL_1: 63;



 A2: 0 <= (c ^2 ) by XREAL_1: 63;

 (d ^2 ) <= ((a ^2 ) + (d ^2 )) by XREAL_1: 31, XREAL_1: 63;

 then ( 0 + (d ^2 )) <= (((a ^2 ) + (d ^2 )) + (c ^2 )) by A2, XREAL_1: 7;

 then ( 0 + (d ^2 )) <= ((b ^2 ) + (((a ^2 ) + (d ^2 )) + (c ^2 ))) by A1, XREAL_1: 7;

 hence thesis;

 end;



 Lm29: a >= (b ^2 ) implies ( sqrt a) >= b

 proof

 assume

 A1: a >= (b ^2 );

 (b ^2 ) >= 0 by XREAL_1: 63;

 then

 A2: ( sqrt a) >= ( sqrt (b ^2 )) by A1, SQUARE_1: 26;

 per cases ;

 suppose b >= 0 ;

 hence thesis by A2, SQUARE_1: 22;

 end;

 suppose

 A3: b < 0 ;

 then ( sqrt a) >= ( - b) by A2, SQUARE_1: 23;

 hence thesis by A3;

 end;

 end;



 Lm30: for a1,a2,a3,a4,a5,a6,b1,b2,b3,b4,b5,b6 be Real st a1 >= b1 & a2 >= b2 & a3 >= b3 & a4 >= b4 & a5 >= b5 & a6 >= b6 holds (((((a1 + a2) + a3) + a4) + a5) + a6) >= (((((b1 + b2) + b3) + b4) + b5) + b6)

 proof

 let a1,a2,a3,a4,a5,a6,b1,b2,b3,b4,b5,b6 be Real;

 assume that

 A1: a1 >= b1 and

 A2: a2 >= b2 and

 A3: a3 >= b3 and

 A4: a4 >= b4 and

 A5: a5 >= b5 and

 A6: a6 >= b6;



 A7: (a1 + a2) >= (b1 + b2) by A1, A2, XREAL_1: 7;



 A8: (a3 + a4) >= (b3 + b4) by A3, A4, XREAL_1: 7;



 A9: (a5 + a6) >= (b5 + b6) by A5, A6, XREAL_1: 7;

 ((a1 + a2) + (a3 + a4)) >= ((b1 + b2) + (b3 + b4)) by A7, A8, XREAL_1: 7;

 then (((a1 + a2) + (a3 + a4)) + (a5 + a6)) >= (((b1 + b2) + (b3 + b4)) + (b5 + b6)) by A9, XREAL_1: 7;

 hence thesis;

 end;



 Lm31: a >= 0 & b >= 0 & (a ^2 ) >= (b ^2 ) implies a >= b

 proof

 assume that

 A1: a >= 0 and

 A2: b >= 0 and

 A3: (a ^2 ) >= (b ^2 );

 ( sqrt (a ^2 )) >= ( sqrt (b ^2 )) by A2, A3, SQUARE_1: 26;

 then a >= ( sqrt (b ^2 )) by A1, SQUARE_1: 22;

 hence thesis by A1, SQUARE_1: 22;

 end;



 Lm32: for m1,m2,m4,m3,n1,n2,n3,n4 be Real holds ((( sqrt ((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 ))) + ( sqrt ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )))) ^2 ) = (((((((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) + (n1 ^2 )) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )) + (2 * ( sqrt (((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) * ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 ))))))

 proof

 let m1,m2,m4,m3,n1,n2,n3,n4 be Real;

 set a = ((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )), b = ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 ));



 A1: a >= 0 by Th67;



 A2: b >= 0 by Th67;

 ((( sqrt a) + ( sqrt b)) ^2 ) = (((( sqrt a) ^2 ) + ((2 * ( sqrt a)) * ( sqrt b))) + (( sqrt b) ^2 ))

 .= ((a + ((2 * ( sqrt a)) * ( sqrt b))) + (( sqrt b) ^2 )) by A1, SQUARE_1:def 2

 .= ((a + (2 * (( sqrt a) * ( sqrt b)))) + b) by A2, SQUARE_1:def 2

 .= ((a + (2 * ( sqrt (a * b)))) + b) by A1, A2, SQUARE_1: 29;

 hence thesis;

 end;



 Lm33: for m1,m2,m3,m4,n1,n2,n3,n4 be Real holds (( sqrt (((((m1 + n1) ^2 ) + ((m2 + n2) ^2 )) + ((m3 + n3) ^2 )) + ((m4 + n4) ^2 ))) ^2 ) = (((((m1 + n1) ^2 ) + ((m2 + n2) ^2 )) + ((m3 + n3) ^2 )) + ((m4 + n4) ^2 ))

 proof

 let m1,m2,m3,m4,n1,n2,n3,n4 be Real;

 (((((m1 + n1) ^2 ) + ((m2 + n2) ^2 )) + ((m3 + n3) ^2 )) + ((m4 + n4) ^2 )) >= 0 by Th67;

 hence thesis by SQUARE_1:def 2;

 end;

 theorem :: QUATERNI:75

 ( Rea z) <= |.z.|

 proof

 0 <= (( Rea z) ^2 ) by XREAL_1: 63;

 then

 A1: ( sqrt (( Rea z) ^2 )) <= ( sqrt ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 ))) by Lm26, SQUARE_1: 26;

 per cases ;

 suppose ( Rea z) >= 0 ;

 hence thesis by A1, SQUARE_1: 22;

 end;

 suppose

 A2: ( Rea z) < 0 ;

 then ( - ( Rea z)) <= |.z.| by A1, SQUARE_1: 23;

 hence thesis by A2;

 end;

 end;

 theorem :: QUATERNI:76

 ( Im1 z) <= |.z.|

 proof

 0 <= (( Im1 z) ^2 ) by XREAL_1: 63;

 then

 A1: ( sqrt (( Im1 z) ^2 )) <= ( sqrt ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 ))) by Lm26, SQUARE_1: 26;

 per cases ;

 suppose ( Im1 z) >= 0 ;

 hence thesis by A1, SQUARE_1: 22;

 end;

 suppose

 A2: ( Im1 z) < 0 ;

 then ( - ( Im1 z)) <= |.z.| by A1, SQUARE_1: 23;

 hence thesis by A2;

 end;

 end;

 theorem :: QUATERNI:77

 ( Im2 z) <= |.z.|

 proof

 0 <= (( Im2 z) ^2 ) by XREAL_1: 63;

 then

 A1: ( sqrt (( Im2 z) ^2 )) <= ( sqrt ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 ))) by Lm27, SQUARE_1: 26;

 per cases ;

 suppose ( Im2 z) >= 0 ;

 hence thesis by A1, SQUARE_1: 22;

 end;

 suppose

 A2: ( Im2 z) < 0 ;

 then ( - ( Im2 z)) <= |.z.| by A1, SQUARE_1: 23;

 hence thesis by A2;

 end;

 end;

 theorem :: QUATERNI:78

 ( Im3 z) <= |.z.|

 proof

 0 <= (( Im3 z) ^2 ) by XREAL_1: 63;

 then

 A1: ( sqrt (( Im3 z) ^2 )) <= ( sqrt ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 ))) by Lm28, SQUARE_1: 26;

 per cases ;

 suppose ( Im3 z) >= 0 ;

 hence thesis by A1, SQUARE_1: 22;

 end;

 suppose

 A2: ( Im3 z) < 0 ;

 then ( - ( Im3 z)) <= |.z.| by A1, SQUARE_1: 23;

 hence thesis by A2;

 end;

 end;

 theorem :: QUATERNI:79



 Th72: |.(z1 + z2).| <= ( |.z1.| + |.z2.|)

 proof

 set m1 = ( Rea z1), m2 = ( Im1 z1), m3 = ( Im2 z1), m4 = ( Im3 z1), n1 = ( Rea z2), n2 = ( Im1 z2), n3 = ( Im2 z2), n4 = ( Im3 z2), a = ((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )), b = ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 ));



 A1: |.z1.| >= 0 by Th60;

 |.z2.| >= 0 by Th60;

 then

 A2: ( |.z1.| + |.z2.|) >= 0 by A1;



 A3: ((( sqrt ((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 ))) + ( sqrt ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )))) ^2 ) = (((((((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) + (n1 ^2 )) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )) + (2 * ( sqrt (((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) * ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )))))) by Lm32;



 A4: (( sqrt (((((m1 + n1) ^2 ) + ((m2 + n2) ^2 )) + ((m3 + n3) ^2 )) + ((m4 + n4) ^2 ))) ^2 ) = (((((m1 + n1) ^2 ) + ((m2 + n2) ^2 )) + ((m3 + n3) ^2 )) + ((m4 + n4) ^2 )) by Lm33;



 A5: ( Rea (z1 + z2)) = (( Rea z1) + ( Rea z2)) by Th29;



 A6: ( Im1 (z1 + z2)) = (( Im1 z1) + ( Im1 z2)) by Th29;



 A7: ( Im2 (z1 + z2)) = (( Im2 z1) + ( Im2 z2)) by Th29;



 A8: ( Im3 (z1 + z2)) = (( Im3 z1) + ( Im3 z2)) by Th29;



 A9: (((m1 * n2) ^2 ) + ((m2 * n1) ^2 )) >= ((2 * (m1 * n2)) * (m2 * n1)) by SERIES_3: 6;



 A10: (((m1 * n3) ^2 ) + ((m3 * n1) ^2 )) >= ((2 * (m1 * n3)) * (m3 * n1)) by SERIES_3: 6;



 A11: (((m1 * n4) ^2 ) + ((m4 * n1) ^2 )) >= ((2 * (m1 * n4)) * (m4 * n1)) by SERIES_3: 6;



 A12: (((m2 * n3) ^2 ) + ((m3 * n2) ^2 )) >= ((2 * (m2 * n3)) * (m3 * n2)) by SERIES_3: 6;



 A13: (((m2 * n4) ^2 ) + ((m4 * n2) ^2 )) >= ((2 * (m2 * n4)) * (m4 * n2)) by SERIES_3: 6;



 A14: (((m3 * n4) ^2 ) + ((m4 * n3) ^2 )) >= ((2 * (m3 * n4)) * (m4 * n3)) by SERIES_3: 6;

 set a1 = ((m1 * n2) ^2 ), a2 = ((m2 * n1) ^2 ), a3 = ((m1 * n3) ^2 ), a4 = ((m3 * n1) ^2 ), a5 = ((m1 * n4) ^2 ), a6 = ((m4 * n1) ^2 ), a7 = ((m2 * n3) ^2 ), a8 = ((m3 * n2) ^2 ), a9 = ((m2 * n4) ^2 ), a10 = ((m4 * n2) ^2 ), a11 = ((m3 * n4) ^2 ), a12 = ((m4 * n3) ^2 ), b1 = ((2 * (m1 * n2)) * (m2 * n1)), b2 = ((2 * (m1 * n3)) * (m3 * n1)), b3 = ((2 * (m1 * n4)) * (m4 * n1)), b4 = ((2 * (m2 * n3)) * (m3 * n2)), b5 = ((2 * (m2 * n4)) * (m4 * n2)), b6 = ((2 * (m3 * n4)) * (m4 * n3));

 ((((((a1 + a2) + (a3 + a4)) + (a5 + a6)) + (a7 + a8)) + (a9 + a10)) + (a11 + a12)) >= (((((b1 + b2) + b3) + b4) + b5) + b6) by A9, A10, A11, A12, A13, A14, Lm30;

 then ((((((((((((a1 + a2) + a3) + a4) + a5) + a6) + a7) + a8) + a9) + a10) + a11) + a12) + (((((m1 * n1) ^2 ) + ((m2 * n2) ^2 )) + ((m3 * n3) ^2 )) + ((m4 * n4) ^2 ))) >= ((((((b1 + b2) + b3) + b4) + b5) + b6) + (((((m1 * n1) ^2 ) + ((m2 * n2) ^2 )) + ((m3 * n3) ^2 )) + ((m4 * n4) ^2 ))) by XREAL_1: 6;

 then ((((((((((((a1 + a2) + a3) + a4) + a5) + a6) + a7) + a8) + a9) + a10) + a11) + a12) + (((((m1 * n1) ^2 ) + ((m2 * n2) ^2 )) + ((m3 * n3) ^2 )) + ((m4 * n4) ^2 ))) >= (((((m1 * n1) + (m2 * n2)) + (m3 * n3)) + (m4 * n4)) ^2 );

 then ( sqrt (((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) * ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )))) >= ((((m1 * n1) + (m2 * n2)) + (m3 * n3)) + (m4 * n4)) by Lm29;

 then (2 * ( sqrt (((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) * ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 ))))) >= (2 * ((((m1 * n1) + (m2 * n2)) + (m3 * n3)) + (m4 * n4))) by XREAL_1: 64;

 then ((a + b) + (2 * ( sqrt (((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) * ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )))))) >= ((a + b) + (2 * ((((m1 * n1) + (m2 * n2)) + (m3 * n3)) + (m4 * n4)))) by XREAL_1: 6;

 hence thesis by A2, A3, A4, A5, A6, A7, A8, Lm31;

 end;

 theorem :: QUATERNI:80



 Th73: |.(z1 - z2).| <= ( |.z1.| + |.z2.|)

 proof

 |.(z1 - z2).| <= ( |.z1.| + |.( - z2).|) by Th72;

 hence thesis by Th65;

 end;



 Lm34: z1 = ((z1 + z2) - z2)

 proof



 A1: z1 = [*( Rea z1), ( Im1 z1), ( Im2 z1), ( Im3 z1)*] by Th17;



 A2: z2 = [*( Rea z2), ( Im1 z2), ( Im2 z2), ( Im3 z2)*] by Th17;



 A3: ( - z2) = [*( - ( Rea z2)), ( - ( Im1 z2)), ( - ( Im2 z2)), ( - ( Im3 z2))*] by Th55;

 (z1 + z2) = [*(( Rea z1) + ( Rea z2)), (( Im1 z1) + ( Im1 z2)), (( Im2 z1) + ( Im2 z2)), (( Im3 z1) + ( Im3 z2))*] by A1, A2, Def6;

 then ((z1 + z2) - z2) = [*((( Rea z1) + ( Rea z2)) - ( Rea z2)), ((( Im1 z1) + ( Im1 z2)) - ( Im1 z2)), ((( Im2 z1) + ( Im2 z2)) - ( Im2 z2)), ((( Im3 z1) + ( Im3 z2)) - ( Im3 z2))*] by A3, Def6;

 hence thesis by Th17;

 end;



 Lm35: z1 = ((z1 - z2) + z2)

 proof



 A1: z1 = [*( Rea z1), ( Im1 z1), ( Im2 z1), ( Im3 z1)*] by Th17;



 A2: z2 = [*( Rea z2), ( Im1 z2), ( Im2 z2), ( Im3 z2)*] by Th17;

 ( - z2) = [*( - ( Rea z2)), ( - ( Im1 z2)), ( - ( Im2 z2)), ( - ( Im3 z2))*] by Th55;

 then (z1 - z2) = [*(( Rea z1) + ( - ( Rea z2))), (( Im1 z1) + ( - ( Im1 z2))), (( Im2 z1) + ( - ( Im2 z2))), (( Im3 z1) + ( - ( Im3 z2)))*] by A1, Def6;



 then ((z1 - z2) + z2) = [*((( Rea z1) + ( - ( Rea z2))) + ( Rea z2)), ((( Im1 z1) + ( - ( Im1 z2))) + ( Im1 z2)), ((( Im2 z1) + ( - ( Im2 z2))) + ( Im2 z2)), ((( Im3 z1) + ( - ( Im3 z2))) + ( Im3 z2))*] by A2, Def6

 .= [*((( Rea z1) + ( Rea z2)) - ( Rea z2)), ((( Im1 z1) + ( Im1 z2)) - ( Im1 z2)), ((( Im2 z1) + ( Im2 z2)) - ( Im2 z2)), ((( Im3 z1) + ( Im3 z2)) - ( Im3 z2))*];

 hence thesis by Th17;

 end;



 Lm36: (z1 - z2) = [*(( Rea z1) - ( Rea z2)), (( Im1 z1) - ( Im1 z2)), (( Im2 z1) - ( Im2 z2)), (( Im3 z1) - ( Im3 z2))*]

 proof



 A1: z1 = [*( Rea z1), ( Im1 z1), ( Im2 z1), ( Im3 z1)*] by Th17;

 ( - z2) = [*( - ( Rea z2)), ( - ( Im1 z2)), ( - ( Im2 z2)), ( - ( Im3 z2))*] by Th55;

 hence thesis by A1, Def6;

 end;



 Lm37: (z1 - z2) = ( - (z2 - z1))

 proof



 A1: ( Rea (z2 - z1)) = (( Rea z2) - ( Rea z1)) by Th35;



 A2: ( Im1 (z2 - z1)) = (( Im1 z2) - ( Im1 z1)) by Th35;



 A3: ( Im2 (z2 - z1)) = (( Im2 z2) - ( Im2 z1)) by Th35;



 A4: ( Im3 (z2 - z1)) = (( Im3 z2) - ( Im3 z1)) by Th35;



 A5: ( Rea ( - (z2 - z1))) = ( - (( Rea z2) - ( Rea z1))) by A1, Th34;



 A6: ( Im1 ( - (z2 - z1))) = ( - (( Im1 z2) - ( Im1 z1))) by A2, Th34;



 A7: ( Im2 ( - (z2 - z1))) = ( - (( Im2 z2) - ( Im2 z1))) by A3, Th34;



 A8: ( Im3 ( - (z2 - z1))) = ( - (( Im3 z2) - ( Im3 z1))) by A4, Th34;



 A9: ( Rea (z1 - z2)) = (( Rea z1) - ( Rea z2)) by Th35;



 A10: ( Im1 (z1 - z2)) = (( Im1 z1) - ( Im1 z2)) by Th35;



 A11: ( Im2 (z1 - z2)) = (( Im2 z1) - ( Im2 z2)) by Th35;

 ( Im3 (z1 - z2)) = (( Im3 z1) - ( Im3 z2)) by Th35;

 hence thesis by Th18, A9, A10, A11, A5, A6, A7, A8;

 end;



 Lm38: (z1 - z2) = 0 implies z1 = z2

 proof

 assume

 A1: (z1 - z2) = 0 ;



 A2: ( Rea (z1 - z2)) = (( Rea z1) - ( Rea z2)) by Th35;



 A3: ( Im1 (z1 - z2)) = (( Im1 z1) - ( Im1 z2)) by Th35;



 A4: ( Im2 (z1 - z2)) = (( Im2 z1) - ( Im2 z2)) by Th35;



 A5: ( Im3 (z1 - z2)) = (( Im3 z1) - ( Im3 z2)) by Th35;



 A6: ( Rea (z1 - z2)) = 0 by A1, Lm6, Th16;



 A7: ( Im1 (z1 - z2)) = 0 by A1, Lm6, Th16;



 A8: ( Im2 (z1 - z2)) = 0 by A1, Lm6, Th16;

 ( Im3 (z1 - z2)) = 0 by A1, Lm6, Th16;

 hence thesis by A2, A3, A4, A5, A6, A7, A8, Th18;

 end;

 theorem :: QUATERNI:81

 ( |.z1.| - |.z2.|) <= |.(z1 + z2).|

 proof

 z1 = ((z1 + z2) - z2) by Lm34;

 then |.z1.| <= ( |.(z1 + z2).| + |.z2.|) by Th73;

 hence thesis by XREAL_1: 20;

 end;

 theorem :: QUATERNI:82



 Th75: ( |.z1.| - |.z2.|) <= |.(z1 - z2).|

 proof

 z1 = ((z1 - z2) + z2) by Lm35;

 then |.z1.| <= ( |.(z1 - z2).| + |.z2.|) by Th72;

 hence thesis by XREAL_1: 20;

 end;

 theorem :: QUATERNI:83



 Th76: |.(z1 - z2).| = |.(z2 - z1).|

 proof



 thus |.(z1 - z2).| = |.( - (z2 - z1)).| by Lm37

 .= |.(z2 - z1).| by Th65;

 end;

 theorem :: QUATERNI:84

 |.(z1 - z2).| = 0 iff z1 = z2

 proof

 thus |.(z1 - z2).| = 0 implies z1 = z2 by Lm38, Th59;

 assume z1 = z2;



 then (z1 - z2) = [*(( Rea z1) - ( Rea z1)), (( Im1 z1) - ( Im1 z1)), (( Im2 z1) - ( Im2 z1)), (( Im3 z1) - ( Im3 z1))*] by Lm36

 .= 0 by Lm6;

 hence thesis by Th58;

 end;



 Lm39: for z,z1,z2 be Quaternion holds (z1 - z2) = ((z1 - z) + (z - z2))

 proof

 let z,z1,z2 be Quaternion;



 A1: ( Rea ((z1 - z) + (z - z2))) = (( Rea (z1 - z)) + ( Rea (z - z2))) by Lm12

 .= (( Rea (z1 - z)) + (( Rea z) - ( Rea z2))) by Th35

 .= ((( Rea z1) - ( Rea z)) + (( Rea z) - ( Rea z2))) by Th35

 .= (( Rea z1) - ( Rea z2))

 .= ( Rea (z1 - z2)) by Th35;



 A2: ( Im1 ((z1 - z) + (z - z2))) = (( Im1 (z1 - z)) + ( Im1 (z - z2))) by Lm12

 .= (( Im1 (z1 - z)) + (( Im1 z) - ( Im1 z2))) by Th35

 .= ((( Im1 z1) - ( Im1 z)) + (( Im1 z) - ( Im1 z2))) by Th35

 .= (( Im1 z1) - ( Im1 z2))

 .= ( Im1 (z1 - z2)) by Th35;



 A3: ( Im2 ((z1 - z) + (z - z2))) = (( Im2 (z1 - z)) + ( Im2 (z - z2))) by Lm12

 .= (( Im2 (z1 - z)) + (( Im2 z) - ( Im2 z2))) by Th35

 .= ((( Im2 z1) - ( Im2 z)) + (( Im2 z) - ( Im2 z2))) by Th35

 .= (( Im2 z1) - ( Im2 z2))

 .= ( Im2 (z1 - z2)) by Th35;

 ( Im3 ((z1 - z) + (z - z2))) = (( Im3 (z1 - z)) + ( Im3 (z - z2))) by Lm12

 .= (( Im3 (z1 - z)) + (( Im3 z) - ( Im3 z2))) by Th35

 .= ((( Im3 z1) - ( Im3 z)) + (( Im3 z) - ( Im3 z2))) by Th35

 .= (( Im3 z1) - ( Im3 z2))

 .= ( Im3 (z1 - z2)) by Th35;

 hence thesis by A1, A2, A3, Th18;

 end;

 theorem :: QUATERNI:85

 |.(z1 - z2).| <= ( |.(z1 - z).| + |.(z - z2).|)

 proof

 |.(z1 - z2).| = |.((z1 - z) + (z - z2)).| by Lm39;

 hence thesis by Th72;

 end;

 theorem :: QUATERNI:86

 |.( |.z1.| - |.z2.|).| <= |.(z1 - z2).|

 proof

 ( |.z2.| - |.z1.|) <= |.(z2 - z1).| by Th75;

 then ( - ( |.z1.| - |.z2.|)) <= |.(z1 - z2).| by Th76;

 then

 A1: ( - |.(z1 - z2).|) <= ( - ( - ( |.z1.| - |.z2.|))) by XREAL_1: 24;

 ( |.z1.| - |.z2.|) <= |.(z1 - z2).| by Th75;

 hence thesis by A1, ABSVALUE: 5;

 end;

 theorem :: QUATERNI:87



 Th80: |.(z1 * z2).| = ( |.z1.| * |.z2.|)

 proof

 set m1 = ( Rea z1), m2 = ( Im1 z1), m3 = ( Im2 z1), m4 = ( Im3 z1), n1 = ( Rea z2), n2 = ( Im1 z2), n3 = ( Im2 z2), n4 = ( Im3 z2);



 A1: ( Rea (z1 * z2)) = ((((m1 * n1) - (m2 * n2)) - (m3 * n3)) - (m4 * n4)) by Lm17;



 A2: ( Im1 (z1 * z2)) = ((((m1 * n2) + (m2 * n1)) + (m3 * n4)) - (m4 * n3)) by Lm17;



 A3: ( Im2 (z1 * z2)) = ((((m1 * n3) + (m3 * n1)) + (m4 * n2)) - (m2 * n4)) by Lm17;



 A4: ( Im3 (z1 * z2)) = ((((m1 * n4) + (m4 * n1)) + (m2 * n3)) - (m3 * n2)) by Lm17;

 set b1 = ((((m1 * n1) - (m2 * n2)) - (m3 * n3)) - (m4 * n4)), b2 = ((((m1 * n2) + (m2 * n1)) + (m3 * n4)) - (m4 * n3)), b3 = ((((m1 * n3) + (m3 * n1)) + (m4 * n2)) - (m2 * n4)), b4 = ((((m1 * n4) + (m4 * n1)) + (m2 * n3)) - (m3 * n2));



 A5: ((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) >= 0 by Th67;



 A6: ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 )) >= 0 by Th67;

 ( sqrt ((((b1 ^2 ) + (b2 ^2 )) + (b3 ^2 )) + (b4 ^2 ))) = ( sqrt (((((m1 ^2 ) + (m2 ^2 )) + (m3 ^2 )) + (m4 ^2 )) * ((((n1 ^2 ) + (n2 ^2 )) + (n3 ^2 )) + (n4 ^2 ))));

 hence thesis by A1, A2, A3, A4, A5, A6, SQUARE_1: 29;

 end;

 theorem :: QUATERNI:88

 |.(z * z).| = ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 ))

 proof



 A1: ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )) >= 0 by Th67;

 ( |.z.| * |.z.|) = (( sqrt ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 ))) ^2 )

 .= ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )) by A1, SQUARE_1:def 2;

 hence thesis by Th80;

 end;

 theorem :: QUATERNI:89

 |.(z * z).| = |.(z * (z *' )).|

 proof



 thus |.(z * z).| = ( |.z.| * |.z.|) by Th80

 .= ( |.z.| * |.(z *' ).|) by Th66

 .= |.(z * (z *' )).| by Th80;

 end;

 theorem :: QUATERNI:90

 z is real implies ( Rea z) = z & ( Im1 z) = 0 & ( Im2 z) = 0 & ( Im3 z) = 0 by Lm18;

 theorem :: QUATERNI:91

 for x,y be Element of REAL holds [*x, y, 0 , 0 *] = [*x, y*] by Lm3;

 theorem :: QUATERNI:92

 (z1 + z2) = ((((( Rea z1) + ( Rea z2)) + ((( Im1 z1) + ( Im1 z2)) * )) + ((( Im2 z1) + ( Im2 z2)) * <j> )) + ((( Im3 z1) + ( Im3 z2)) * <k> )) by Lm20;

 theorem :: QUATERNI:93

 (z1 * z2) = (((((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))) + (((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))) * )) + (((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2))) * <j> )) + (((((( Rea z1) * ( Im3 z2)) + (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2))) * <k> )) by Lm21;

 theorem :: QUATERNI:94

 ( - z) = (((( - ( Rea z)) + (( - ( Im1 z)) * )) + (( - ( Im2 z)) * <j> )) + (( - ( Im3 z)) * <k> )) by Lm24;

 theorem :: QUATERNI:95

 (z1 - z2) = ((((( Rea z1) - ( Rea z2)) + ((( Im1 z1) - ( Im1 z2)) * )) + ((( Im2 z1) - ( Im2 z2)) * <j> )) + ((( Im3 z1) - ( Im3 z2)) * <k> )) by Lm25;

 theorem :: QUATERNI:96

 for a,b,c,d be Real st ((((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 )) = 0 holds a = 0 & b = 0 & c = 0 & d = 0 by Lm9;

 theorem :: QUATERNI:97

 ( Rea (z1 * z2)) = ((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))) & ( Im1 (z1 * z2)) = ((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))) & ( Im2 (z1 * z2)) = ((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2))) & ( Im3 (z1 * z2)) = ((((( Rea z1) * ( Im3 z2)) + (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2))) by Lm17;