quatern3.miz

begin

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

 theorem :: QUATERN3:1



 Th1: ( Rea (z1 * z2)) = ( Rea (z2 * z1))

 proof

 ( Rea (z2 * z1)) = ((((( Rea z2) * ( Rea z1)) - (( Im1 z2) * ( Im1 z1))) - (( Im2 z2) * ( Im2 z1))) - (( Im3 z2) * ( Im3 z1))) by QUATERNI: 97;

 hence thesis by QUATERNI: 97;

 end;



 Lm1: z is Real implies z = ( Rea z) & ( Im1 z) = 0 & ( Im2 z) = 0 & ( Im3 z) = 0

 proof

 assume z is Real;

 then

 reconsider x = z as Element of REAL by XREAL_0:def 1;

 x = [*x, ( In ( 0 , REAL ))*] & [*x, ( In ( 0 , REAL ))*] = [*x, 0 , 0 , 0 *] by ARYTM_0:def 5, QUATERNI: 91;

 hence thesis by QUATERNI: 23;

 end;

 theorem :: QUATERN3:2

 z is Real implies (z + z3) = ((((( Rea z) + ( Rea z3)) + (( Im1 z3) * )) + (( Im2 z3) * <j> )) + (( Im3 z3) * <k> ))

 proof

 reconsider z1 = (z + z3) as Quaternion;

 assume

 A1: z is Real;

 then

 A2: ( Im3 z) = 0 by Lm1;

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



 A3: ( Rea z2) = (( Rea z) + ( Rea z3)) by QUATERNI: 23

 .= ( Rea z1) by QUATERNI: 36;



 A4: ( Im1 z2) = (( Im1 z) + ( Im1 z3)) by QUATERNI: 23

 .= ( Im1 z1) by QUATERNI: 36;



 A5: ( Im3 z2) = (( Im3 z) + ( Im3 z3)) by QUATERNI: 23

 .= ( Im3 z1) by QUATERNI: 36;



 A6: ( Im2 z2) = (( Im2 z) + ( Im2 z3)) by QUATERNI: 23

 .= ( Im2 z1) by QUATERNI: 36;

 ( Im1 z) = 0 & ( Im2 z) = 0 by A1, Lm1;

 then (z + z3) = [*(( Rea z) + ( Rea z3)), ( Im1 z3), ( Im2 z3), ( Im3 z3)*] by A2, A3, A4, A6, A5, QUATERNI: 25;

 hence thesis by QUATERN2: 1;

 end;

 theorem :: QUATERN3:3

 z is Real implies (z - z3) = [*(( Rea z) - ( Rea z3)), ( - ( Im1 z3)), ( - ( Im2 z3)), ( - ( Im3 z3))*]

 proof

 reconsider z1 = (z + ( - z3)) as Quaternion;

 assume

 A1: z is Real;

 then

 A2: ( Im3 z) = 0 by Lm1;

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



 A3: ( Rea z2) = (( Rea z) + ( - ( Rea z3))) by QUATERNI: 23

 .= (( Rea z) + ( Rea ( - z3))) by QUATERNI: 41

 .= ( Rea z1) by QUATERNI: 36;



 A4: ( Im1 z2) = (( Im1 z) + ( - ( Im1 z3))) by QUATERNI: 23

 .= (( Im1 z) + ( Im1 ( - z3))) by QUATERNI: 41

 .= ( Im1 z1) by QUATERNI: 36;



 A5: ( Im3 z2) = (( Im3 z) + ( - ( Im3 z3))) by QUATERNI: 23

 .= (( Im3 z) + ( Im3 ( - z3))) by QUATERNI: 41

 .= ( Im3 z1) by QUATERNI: 36;



 A6: ( Im2 z2) = (( Im2 z) + ( - ( Im2 z3))) by QUATERNI: 23

 .= (( Im2 z) + ( Im2 ( - z3))) by QUATERNI: 41

 .= ( Im2 z1) by QUATERNI: 36;

 ( Im1 z) = 0 & ( Im2 z) = 0 by A1, Lm1;

 hence thesis by A2, A3, A4, A6, A5, QUATERNI: 25;

 end;

 theorem :: QUATERN3:4

 z is Real implies (z * z3) = [*(( Rea z) * ( Rea z3)), (( Rea z) * ( Im1 z3)), (( Rea z) * ( Im2 z3)), (( Rea z) * ( Im3 z3))*]

 proof

 assume

 A1: z is Real;

 then

 A2: ( Im3 z) = 0 by Lm1;



 A3: (z * z3) = [*((((( Rea z) * ( Rea z3)) - (( Im1 z) * ( Im1 z3))) - (( Im2 z) * ( Im2 z3))) - (( Im3 z) * ( Im3 z3))), ((((( Rea z) * ( Im1 z3)) + (( Im1 z) * ( Rea z3))) + (( Im2 z) * ( Im3 z3))) - (( Im3 z) * ( Im2 z3))), ((((( Rea z) * ( Im2 z3)) + (( Im2 z) * ( Rea z3))) + (( Im3 z) * ( Im1 z3))) - (( Im1 z) * ( Im3 z3))), ((((( Rea z) * ( Im3 z3)) + (( Im3 z) * ( Rea z3))) + (( Im1 z) * ( Im2 z3))) - (( Im2 z) * ( Im1 z3)))*]

 proof

 reconsider z9 = (z * z3) as Quaternion;

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



 A4: ( Im1 z1) = ((((( Rea z) * ( Im1 z3)) + (( Im1 z) * ( Rea z3))) + (( Im2 z) * ( Im3 z3))) - (( Im3 z) * ( Im2 z3))) by QUATERNI: 23

 .= ( Im1 z9) by QUATERNI: 97;



 A5: ( Im2 z1) = ((((( Rea z) * ( Im2 z3)) + (( Im2 z) * ( Rea z3))) + (( Im3 z) * ( Im1 z3))) - (( Im1 z) * ( Im3 z3))) by QUATERNI: 23

 .= ( Im2 z9) by QUATERNI: 97;



 A6: ( Im3 z1) = ((((( Rea z) * ( Im3 z3)) + (( Im3 z) * ( Rea z3))) + (( Im1 z) * ( Im2 z3))) - (( Im2 z) * ( Im1 z3))) by QUATERNI: 23

 .= ( Im3 z9) by QUATERNI: 97;

 ( Rea z1) = ((((( Rea z) * ( Rea z3)) - (( Im1 z) * ( Im1 z3))) - (( Im2 z) * ( Im2 z3))) - (( Im3 z) * ( Im3 z3))) by QUATERNI: 23

 .= ( Rea z9) by QUATERNI: 97;

 hence thesis by A4, A5, A6, QUATERNI: 25;

 end;

 ( Im1 z) = 0 & ( Im2 z) = 0 by A1, Lm1;

 hence thesis by A2, A3;

 end;

 theorem :: QUATERN3:5

 z is Real implies (z * ) = [* 0 , ( Rea z), 0 , 0 *]

 proof

 assume

 A1: z is Real;

 then

 reconsider x = z as Real;



 A2: x = ( Rea z) by Lm1;

 (z * ) = [*( Rea (z * )), ( Im1 (z * )), ( Im2 (z * )), ( Im3 (z * ))*] by QUATERNI: 24

 .= [* 0 , ( Im1 (z * )), ( Im2 (z * )), ( Im3 (z * ))*] by A1, QUATERNI: 33

 .= [* 0 , x, ( Im2 (z * )), ( Im3 (z * ))*] by QUATERNI: 33

 .= [* 0 , x, 0 , ( Im3 (z * ))*] by QUATERNI: 33

 .= [* 0 , ( Rea z), 0 , 0 *] by A2, QUATERNI: 33;

 hence thesis;

 end;

 theorem :: QUATERN3:6

 z is Real implies (z * <j> ) = [* 0 , 0 , ( Rea z), 0 *]

 proof

 assume

 A1: z is Real;

 then

 reconsider x = z as Real;



 A2: x = ( Rea z) by Lm1;

 (z * <j> ) = [*( Rea (z * <j> )), ( Im1 (z * <j> )), ( Im2 (z * <j> )), ( Im3 (z * <j> ))*] by QUATERNI: 24

 .= [* 0 , ( Im1 (z * <j> )), ( Im2 (z * <j> )), ( Im3 (z * <j> ))*] by A1, QUATERNI: 34

 .= [* 0 , 0 , ( Im2 (z * <j> )), ( Im3 (z * <j> ))*] by A1, QUATERNI: 34

 .= [* 0 , 0 , x, ( Im3 (z * <j> ))*] by QUATERNI: 34

 .= [* 0 , 0 , ( Rea z), 0 *] by A2, QUATERNI: 34;

 hence thesis;

 end;

 theorem :: QUATERN3:7

 z is Real implies (z * <k> ) = [* 0 , 0 , 0 , ( Rea z)*]

 proof

 assume

 A1: z is Real;

 then

 reconsider x = z as Real;



 A2: x = ( Rea z) by Lm1;

 (z * <k> ) = [*( Rea (z * <k> )), ( Im1 (z * <k> )), ( Im2 (z * <k> )), ( Im3 (z * <k> ))*] by QUATERNI: 24

 .= [* 0 , ( Im1 (z * <k> )), ( Im2 (z * <k> )), ( Im3 (z * <k> ))*] by A1, QUATERNI: 35

 .= [* 0 , 0 , ( Im2 (z * <k> )), ( Im3 (z * <k> ))*] by A1, QUATERNI: 35

 .= [* 0 , 0 , 0 , ( Im3 (z * <k> ))*] by A1, QUATERNI: 35

 .= [* 0 , 0 , 0 , ( Rea z)*] by A2, QUATERNI: 35;

 hence thesis;

 end;

 theorem :: QUATERN3:8

 (z - 0q ) = z

 proof

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

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

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

 .= [* 0 , 0 , 0 , 0 *] by QUATERNI: 91;

 then ( - 0q ) = [*( - 0 ), ( - 0 ), ( - 0 ), ( - 0 )*] by QUATERN2: 4;



 then (z - 0q ) = [*(x + ( - 0 )), (y + ( - 0 )), (w + ( - 0 )), (v + ( - 0 ))*] by A1, QUATERNI:def 7

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

 hence thesis by A1;

 end;

 theorem :: QUATERN3:9

 z is Real implies (z * z1) = (z1 * z)

 proof

 assume

 A1: z is Real;

 then

 A2: ( Im3 z) = 0 by Lm1;



 A3: ( Im1 z) = 0 & ( Im2 z) = 0 by A1, Lm1;

 (z1 * z) = (((((((( Rea z1) * ( Rea z)) - (( Im1 z1) * ( Im1 z))) - (( Im2 z1) * ( Im2 z))) - (( Im3 z1) * ( Im3 z))) + (((((( Rea z1) * ( Im1 z)) + (( Im1 z1) * ( Rea z))) + (( Im2 z1) * ( Im3 z))) - (( Im3 z1) * ( Im2 z))) * )) + (((((( Rea z1) * ( Im2 z)) + (( Im2 z1) * ( Rea z))) + (( Im3 z1) * ( Im1 z))) - (( Im1 z1) * ( Im3 z))) * <j> )) + (((((( Rea z1) * ( Im3 z)) + (( Im3 z1) * ( Rea z))) + (( Im1 z1) * ( Im2 z))) - (( Im2 z1) * ( Im1 z))) * <k> )) by QUATERNI: 93;

 hence thesis by A2, A3, QUATERNI: 93;

 end;

 theorem :: QUATERN3:10

 ( Im1 z) = 0 & ( Im2 z) = 0 & ( Im3 z) = 0 implies z = ( Rea z)

 proof

 set x = ( Rea z);

 assume ( Im1 z) = 0 & ( Im2 z) = 0 & ( Im3 z) = 0 ;

 then

 A1: z = [*x, 0 , 0 , 0 *] by QUATERNI: 24;

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

 [*x, 0 , 0 , 0 *] = [*xx, zz*] by QUATERNI: 91;

 hence thesis by A1, ARYTM_0:def 5;

 end;

 theorem :: QUATERN3:11



 Th11: ( |.z.| ^2 ) = ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 ))

 proof

 ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )) >= 0 by QUATERNI: 74;



 then ( |.z.| ^2 ) = ( sqrt (((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )) ^2 )) by SQUARE_1: 29

 .= ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )) by QUATERNI: 74, SQUARE_1: 22;

 hence thesis;

 end;

 theorem :: QUATERN3:12

 ( |.z.| ^2 ) = |.(z * (z *' )).|

 proof

 |.(z * z).| = |.(z * (z *' )).| & ( |.z.| ^2 ) = ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )) by Th11, QUATERNI: 89;

 hence thesis by QUATERNI: 88;

 end;

 theorem :: QUATERN3:13

 ( |.z.| ^2 ) = ( Rea (z * (z *' )))

 proof

 ( Rea (z * (z *' ))) = ((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )) by QUATERNI: 60;

 hence thesis by Th11;

 end;

 theorem :: QUATERN3:14

 (2 * ( Rea z)) = ( Rea (z + (z *' )))

 proof

 z = [*( Rea z), ( Im1 z), ( Im2 z), ( Im3 z)*] & (z *' ) = [*( Rea z), ( - ( Im1 z)), ( - ( Im2 z)), ( - ( Im3 z))*] by QUATERNI: 24, QUATERNI: 43;



 then (z + (z *' )) = [*(( Rea z) + ( Rea z)), (( Im1 z) + ( - ( Im1 z))), (( Im2 z) + ( - ( Im2 z))), (( Im3 z) + ( - ( Im3 z)))*] by QUATERNI:def 7

 .= [*(2 * ( Rea z)), 0 , 0 , 0 *];

 hence thesis by QUATERNI: 23;

 end;

 theorem :: QUATERN3:15

 z is Real implies ((z * z1) *' ) = ((z *' ) * (z1 *' ))

 proof



 A1: ( Im1 (z1 *' )) = ( - ( Im1 z1)) & ( Im2 (z1 *' )) = ( - ( Im2 z1)) by QUATERNI: 44;



 A2: ( Im3 (z1 *' )) = ( - ( Im3 z1)) & ( Rea (z *' )) = ( Rea z) by QUATERNI: 44;



 A3: ( Rea (z * z1)) = ((((( Rea z) * ( Rea z1)) - (( Im1 z) * ( Im1 z1))) - (( Im2 z) * ( Im2 z1))) - (( Im3 z) * ( Im3 z1))) by QUATERNI: 97;

 assume

 A4: z is Real;

 then

 reconsider x = z as Real;



 A5: ( Im1 z) = 0 & ( Im2 z) = 0 by A4, Lm1;



 A6: ( Im3 z) = 0 by A4, Lm1;



 A7: ( Im3 (z *' )) = ( - ( Im3 z)) by QUATERNI: 44;



 A8: ( Im1 (z *' )) = ( - ( Im1 z)) & ( Im2 (z *' )) = ( - ( Im2 z)) by QUATERNI: 44;



 A9: ( Im3 (z * z1)) = ((((( Rea z) * ( Im3 z1)) + (( Im3 z) * ( Rea z1))) + (( Im1 z) * ( Im2 z1))) - (( Im2 z) * ( Im1 z1))) by QUATERNI: 97;



 A10: ( Im2 (z * z1)) = ((((( Rea z) * ( Im2 z1)) + (( Im2 z) * ( Rea z1))) + (( Im3 z) * ( Im1 z1))) - (( Im1 z) * ( Im3 z1))) by QUATERNI: 97;



 A11: ( Im1 (z * z1)) = ((((( Rea z) * ( Im1 z1)) + (( Im1 z) * ( Rea z1))) + (( Im2 z) * ( Im3 z1))) - (( Im3 z) * ( Im2 z1))) by QUATERNI: 97;

 set z3 = (z *' ), z2 = (z1 *' );



 A12: (z3 * z2) = (((((((( Rea z3) * ( Rea z2)) - (( Im1 z3) * ( Im1 z2))) - (( Im2 z3) * ( Im2 z2))) - (( Im3 z3) * ( Im3 z2))) + (((((( Rea z3) * ( Im1 z2)) + (( Im1 z3) * ( Rea z2))) + (( Im2 z3) * ( Im3 z2))) - (( Im3 z3) * ( Im2 z2))) * )) + (((((( Rea z3) * ( Im2 z2)) + (( Im2 z3) * ( Rea z2))) + (( Im3 z3) * ( Im1 z2))) - (( Im1 z3) * ( Im3 z2))) * <j> )) + (((((( Rea z3) * ( Im3 z2)) + (( Im3 z3) * ( Rea z2))) + (( Im1 z3) * ( Im2 z2))) - (( Im2 z3) * ( Im1 z2))) * <k> )) by QUATERNI: 93;

 ((z * z1) *' ) = (((( Rea ((z * z1) *' )) + (( Im1 ((z * z1) *' )) * )) + (( Im2 ((z * z1) *' )) * <j> )) + (( Im3 ((z * z1) *' )) * <k> )) by QUATERNI: 37

 .= (((((((( Rea z) * ( Rea z1)) - (( Im1 z) * ( Im1 z1))) - (( Im2 z) * ( Im2 z1))) - (( Im3 z) * ( Im3 z1))) + (( Im1 ((z * z1) *' )) * )) + (( Im2 ((z * z1) *' )) * <j> )) + (( Im3 ((z * z1) *' )) * <k> )) by A3, QUATERNI: 44

 .= (((((((( Rea z) * ( Rea z1)) - (( Im1 z) * ( Im1 z1))) - (( Im2 z) * ( Im2 z1))) - (( Im3 z) * ( Im3 z1))) + (( - ((((( Rea z) * ( Im1 z1)) + (( Im1 z) * ( Rea z1))) + (( Im2 z) * ( Im3 z1))) - (( Im3 z) * ( Im2 z1)))) * )) + (( Im2 ((z * z1) *' )) * <j> )) + (( Im3 ((z * z1) *' )) * <k> )) by A11, QUATERNI: 44

 .= (((((((( Rea z) * ( Rea z1)) - (( Im1 z) * ( Im1 z1))) - (( Im2 z) * ( Im2 z1))) - (( Im3 z) * ( Im3 z1))) + (( - ((((( Rea z) * ( Im1 z1)) + (( Im1 z) * ( Rea z1))) + (( Im2 z) * ( Im3 z1))) - (( Im3 z) * ( Im2 z1)))) * )) + (( - ((((( Rea z) * ( Im2 z1)) + (( Im2 z) * ( Rea z1))) + (( Im3 z) * ( Im1 z1))) - (( Im1 z) * ( Im3 z1)))) * <j> )) + (( Im3 ((z * z1) *' )) * <k> )) by A10, QUATERNI: 44

 .= (((((((( Rea z) * ( Rea z1)) - (( Im1 z) * ( Im1 z1))) - (( Im2 z) * ( Im2 z1))) - (( Im3 z) * ( Im3 z1))) + (( - ((((( Rea z) * ( Im1 z1)) + (( Im1 z) * ( Rea z1))) + (( Im2 z) * ( Im3 z1))) - (( Im3 z) * ( Im2 z1)))) * )) + (( - ((((( Rea z) * ( Im2 z1)) + (( Im2 z) * ( Rea z1))) + (( Im3 z) * ( Im1 z1))) - (( Im1 z) * ( Im3 z1)))) * <j> )) + (( - ((((( Rea z) * ( Im3 z1)) + (( Im3 z) * ( Rea z1))) + (( Im1 z) * ( Im2 z1))) - (( Im2 z) * ( Im1 z1)))) * <k> )) by A9, QUATERNI: 44;

 hence thesis by A5, A6, A1, A2, A8, A7, A12, QUATERNI: 44;

 end;

 theorem :: QUATERN3:16

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

 proof



 A1: ( Rea (z2 *' )) = ( Rea z2) & ( Im1 (z2 *' )) = ( - ( Im1 z2)) by QUATERNI: 44;



 A2: ( Im2 (z2 *' )) = ( - ( Im2 z2)) & ( Im3 (z2 *' )) = ( - ( Im3 z2)) by QUATERNI: 44;



 A3: ( Rea (z1 * z2)) = ((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))) by QUATERNI: 97;



 A4: ( Im3 (z1 * z2)) = ((((( Rea z1) * ( Im3 z2)) + (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2))) by QUATERNI: 97;



 A5: ( Im2 (z1 *' )) = ( - ( Im2 z1)) & ( Im3 (z1 *' )) = ( - ( Im3 z1)) by QUATERNI: 44;



 A6: ( Rea (z1 *' )) = ( Rea z1) & ( Im1 (z1 *' )) = ( - ( Im1 z1)) by QUATERNI: 44;



 A7: ( Im2 (z1 * z2)) = ((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2))) by QUATERNI: 97;



 A8: ( Im1 (z1 * z2)) = ((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))) by QUATERNI: 97;

 set z3 = (z2 *' ), z4 = (z1 *' );



 A9: (z3 * z4) = (((((((( Rea z3) * ( Rea z4)) - (( Im1 z3) * ( Im1 z4))) - (( Im2 z3) * ( Im2 z4))) - (( Im3 z3) * ( Im3 z4))) + (((((( Rea z3) * ( Im1 z4)) + (( Im1 z3) * ( Rea z4))) + (( Im2 z3) * ( Im3 z4))) - (( Im3 z3) * ( Im2 z4))) * )) + (((((( Rea z3) * ( Im2 z4)) + (( Im2 z3) * ( Rea z4))) + (( Im3 z3) * ( Im1 z4))) - (( Im1 z3) * ( Im3 z4))) * <j> )) + (((((( Rea z3) * ( Im3 z4)) + (( Im3 z3) * ( Rea z4))) + (( Im1 z3) * ( Im2 z4))) - (( Im2 z3) * ( Im1 z4))) * <k> )) by QUATERNI: 93;

 ((z1 * z2) *' ) = (((( Rea ((z1 * z2) *' )) + (( Im1 ((z1 * z2) *' )) * )) + (( Im2 ((z1 * z2) *' )) * <j> )) + (( Im3 ((z1 * z2) *' )) * <k> )) by QUATERNI: 37

 .= (((((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))) + (( Im1 ((z1 * z2) *' )) * )) + (( Im2 ((z1 * z2) *' )) * <j> )) + (( Im3 ((z1 * z2) *' )) * <k> )) by A3, QUATERNI: 44

 .= (((((((( 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) *' )) * <j> )) + (( Im3 ((z1 * z2) *' )) * <k> )) by A8, QUATERNI: 44

 .= (((((((( 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> )) + (( Im3 ((z1 * z2) *' )) * <k> )) by A7, QUATERNI: 44

 .= (((((((( 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 A4, QUATERNI: 44;

 hence thesis by A1, A2, A6, A5, A9;

 end;

 theorem :: QUATERN3:17



 Th17: ( |.(z1 * z2).| ^2 ) = (( |.z1.| ^2 ) * ( |.z2.| ^2 ))

 proof

 set z3 = (z1 * z2);



 A1: ( 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))) by QUATERNI: 97;



 A2: ( 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 QUATERNI: 97;

 ( |.z1.| ^2 ) = ((((( Rea z1) ^2 ) + (( Im1 z1) ^2 )) + (( Im2 z1) ^2 )) + (( Im3 z1) ^2 )) & ( |.z2.| ^2 ) = ((((( Rea z2) ^2 ) + (( Im1 z2) ^2 )) + (( Im2 z2) ^2 )) + (( Im3 z2) ^2 )) by Th11;

 hence thesis by A1, A2, Th11;

 end;

 theorem :: QUATERN3:18

 (( * z1) - (z1 * )) = [* 0 , 0 , ( - (2 * ( Im3 z1))), (2 * ( Im2 z1))*]

 proof

 set z = ;

 set s = ((z * z1) - (z1 * z));



 A1: ( Rea (z1 * z)) = ((((( Rea z1) * ( Rea z)) - (( Im1 z1) * ( Im1 z))) - (( Im2 z1) * ( Im2 z))) - (( Im3 z1) * ( Im3 z))) & ( Im1 (z1 * z)) = ((((( Rea z1) * ( Im1 z)) + (( Im1 z1) * ( Rea z))) + (( Im2 z1) * ( Im3 z))) - (( Im3 z1) * ( Im2 z))) & ( Im2 (z1 * z)) = ((((( Rea z1) * ( Im2 z)) + (( Im2 z1) * ( Rea z))) + (( Im3 z1) * ( Im1 z))) - (( Im1 z1) * ( Im3 z))) & ( Im3 (z1 * z)) = ((((( Rea z1) * ( Im3 z)) + (( Im3 z1) * ( Rea z))) + (( Im1 z1) * ( Im2 z))) - (( Im2 z1) * ( Im1 z))) by QUATERNI: 97;



 A2: ( Im2 (z * z1)) = ((((( Rea z) * ( Im2 z1)) + (( Im2 z) * ( Rea z1))) + (( Im3 z) * ( Im1 z1))) - (( Im1 z) * ( Im3 z1))) & ( Im3 (z * z1)) = ((((( Rea z) * ( Im3 z1)) + (( Im3 z) * ( Rea z1))) + (( Im1 z) * ( Im2 z1))) - (( Im2 z) * ( Im1 z1))) by QUATERNI: 97;

 ( Rea (z * z1)) = ( - ( Im1 z1)) & ( Im1 (z * z1)) = ( Rea z1) by A1, QUATERNI: 30, QUATERNI: 97;

 then

 A3: ( Rea s) = (( - ( Im1 z1)) - ( - ( Im1 z1))) & ( Im1 s) = (( Rea z1) - ( Rea z1)) by A1, QUATERNI: 30, QUATERNI: 42;

 ( Im2 s) = (( - ( Im3 z1)) - ( Im3 z1)) & ( Im3 s) = (( Im2 z1) - ( - ( Im2 z1))) by A2, A1, QUATERNI: 30, QUATERNI: 42;

 hence thesis by A3, QUATERNI: 24;

 end;

 theorem :: QUATERN3:19

 (( * z1) + (z1 * )) = [*( - (2 * ( Im1 z1))), (2 * ( Rea z1)), 0 , 0 *]

 proof

 set z = ;



 A1: (z * z1) = (((((((( Rea z) * ( Rea z1)) - (( Im1 z) * ( Im1 z1))) - (( Im2 z) * ( Im2 z1))) - (( Im3 z) * ( Im3 z1))) + (((((( Rea z) * ( Im1 z1)) + (( Im1 z) * ( Rea z1))) + (( Im2 z) * ( Im3 z1))) - (( Im3 z) * ( Im2 z1))) * )) + (((((( Rea z) * ( Im2 z1)) + (( Im2 z) * ( Rea z1))) + (( Im3 z) * ( Im1 z1))) - (( Im1 z) * ( Im3 z1))) * <j> )) + (((((( Rea z) * ( Im3 z1)) + (( Im3 z) * ( Rea z1))) + (( Im1 z) * ( Im2 z1))) - (( Im2 z) * ( Im1 z1))) * <k> )) by QUATERNI: 93

 .= [*( - ( Im1 z1)), ( Rea z1), ( - ( Im3 z1)), ( Im2 z1)*] by QUATERN2: 1, QUATERNI: 30;

 then

 A2: ( Im2 (z * z1)) = ( - ( Im3 z1)) & ( Im3 (z * z1)) = ( Im2 z1) by QUATERNI: 23;



 A3: (z1 * z) = (((((((( Rea z1) * ( Rea z)) - (( Im1 z1) * ( Im1 z))) - (( Im2 z1) * ( Im2 z))) - (( Im3 z1) * ( Im3 z))) + (((((( Rea z1) * ( Im1 z)) + (( Im1 z1) * ( Rea z))) + (( Im2 z1) * ( Im3 z))) - (( Im3 z1) * ( Im2 z))) * )) + (((((( Rea z1) * ( Im2 z)) + (( Im2 z1) * ( Rea z))) + (( Im3 z1) * ( Im1 z))) - (( Im1 z1) * ( Im3 z))) * <j> )) + (((((( Rea z1) * ( Im3 z)) + (( Im3 z1) * ( Rea z))) + (( Im1 z1) * ( Im2 z))) - (( Im2 z1) * ( Im1 z))) * <k> )) by QUATERNI: 93

 .= [*( - ( Im1 z1)), ( Rea z1), ( Im3 z1), ( - ( Im2 z1))*] by QUATERN2: 1, QUATERNI: 30;

 then

 A4: ( Rea (z1 * z)) = ( - ( Im1 z1)) & ( Im1 (z1 * z)) = ( Rea z1) by QUATERNI: 23;



 A5: ( Im2 (z1 * z)) = ( Im3 z1) & ( Im3 (z1 * z)) = ( - ( Im2 z1)) by A3, QUATERNI: 23;

 ( Rea (z * z1)) = ( - ( Im1 z1)) & ( Im1 (z * z1)) = ( Rea z1) by A1, QUATERNI: 23;

 then ((z * z1) + (z1 * z)) = ((((( - ( Im1 z1)) + ( - ( Im1 z1))) + ((( Rea z1) + ( Rea z1)) * )) + ((( - ( Im3 z1)) + ( Im3 z1)) * <j> )) + ((( Im2 z1) + ( - ( Im2 z1))) * <k> )) by A2, A4, A5, QUATERNI: 92;

 hence thesis by QUATERN2: 1;

 end;

 theorem :: QUATERN3:20

 (( <j> * z1) - (z1 * <j> )) = [* 0 , (2 * ( Im3 z1)), 0 , ( - (2 * ( Im1 z1)))*]

 proof

 set z = <j> ;



 A1: (z * z1) = (((((((( Rea z) * ( Rea z1)) - (( Im1 z) * ( Im1 z1))) - (( Im2 z) * ( Im2 z1))) - (( Im3 z) * ( Im3 z1))) + (((((( Rea z) * ( Im1 z1)) + (( Im1 z) * ( Rea z1))) + (( Im2 z) * ( Im3 z1))) - (( Im3 z) * ( Im2 z1))) * )) + (((((( Rea z) * ( Im2 z1)) + (( Im2 z) * ( Rea z1))) + (( Im3 z) * ( Im1 z1))) - (( Im1 z) * ( Im3 z1))) * <j> )) + (((((( Rea z) * ( Im3 z1)) + (( Im3 z) * ( Rea z1))) + (( Im1 z) * ( Im2 z1))) - (( Im2 z) * ( Im1 z1))) * <k> )) by QUATERNI: 93

 .= [*( - ( Im2 z1)), ( Im3 z1), ( Rea z1), ( - ( Im1 z1))*] by QUATERN2: 1, QUATERNI: 31;

 (z1 * z) = (((((((( Rea z1) * ( Rea z)) - (( Im1 z1) * ( Im1 z))) - (( Im2 z1) * ( Im2 z))) - (( Im3 z1) * ( Im3 z))) + (((((( Rea z1) * ( Im1 z)) + (( Im1 z1) * ( Rea z))) + (( Im2 z1) * ( Im3 z))) - (( Im3 z1) * ( Im2 z))) * )) + (((((( Rea z1) * ( Im2 z)) + (( Im2 z1) * ( Rea z))) + (( Im3 z1) * ( Im1 z))) - (( Im1 z1) * ( Im3 z))) * <j> )) + (((((( Rea z1) * ( Im3 z)) + (( Im3 z1) * ( Rea z))) + (( Im1 z1) * ( Im2 z))) - (( Im2 z1) * ( Im1 z))) * <k> )) by QUATERNI: 93

 .= [*( - ( Im2 z1)), ( - ( Im3 z1)), ( Rea z1), ( Im1 z1)*] by QUATERN2: 1, QUATERNI: 31;



 then ((z * z1) - (z1 * z)) = [*(( - ( Im2 z1)) - ( - ( Im2 z1))), (( Im3 z1) - ( - ( Im3 z1))), (( Rea z1) - ( Rea z1)), (( - ( Im1 z1)) - ( Im1 z1))*] by A1, QUATERN2: 5

 .= [* 0 , (2 * ( Im3 z1)), 0 , ( - (2 * ( Im1 z1)))*];

 hence thesis;

 end;

 theorem :: QUATERN3:21

 (( <j> * z1) + (z1 * <j> )) = [*( - (2 * ( Im2 z1))), 0 , (2 * ( Rea z1)), 0 *]

 proof

 set z = <j> ;



 A1: (z * z1) = (((((((( Rea z) * ( Rea z1)) - (( Im1 z) * ( Im1 z1))) - (( Im2 z) * ( Im2 z1))) - (( Im3 z) * ( Im3 z1))) + (((((( Rea z) * ( Im1 z1)) + (( Im1 z) * ( Rea z1))) + (( Im2 z) * ( Im3 z1))) - (( Im3 z) * ( Im2 z1))) * )) + (((((( Rea z) * ( Im2 z1)) + (( Im2 z) * ( Rea z1))) + (( Im3 z) * ( Im1 z1))) - (( Im1 z) * ( Im3 z1))) * <j> )) + (((((( Rea z) * ( Im3 z1)) + (( Im3 z) * ( Rea z1))) + (( Im1 z) * ( Im2 z1))) - (( Im2 z) * ( Im1 z1))) * <k> )) by QUATERNI: 93

 .= [*( - ( Im2 z1)), ( Im3 z1), ( Rea z1), ( - ( Im1 z1))*] by QUATERN2: 1, QUATERNI: 31;

 then

 A2: ( Im2 (z * z1)) = ( Rea z1) & ( Im3 (z * z1)) = ( - ( Im1 z1)) by QUATERNI: 23;



 A3: (z1 * z) = (((((((( Rea z1) * ( Rea z)) - (( Im1 z1) * ( Im1 z))) - (( Im2 z1) * ( Im2 z))) - (( Im3 z1) * ( Im3 z))) + (((((( Rea z1) * ( Im1 z)) + (( Im1 z1) * ( Rea z))) + (( Im2 z1) * ( Im3 z))) - (( Im3 z1) * ( Im2 z))) * )) + (((((( Rea z1) * ( Im2 z)) + (( Im2 z1) * ( Rea z))) + (( Im3 z1) * ( Im1 z))) - (( Im1 z1) * ( Im3 z))) * <j> )) + (((((( Rea z1) * ( Im3 z)) + (( Im3 z1) * ( Rea z))) + (( Im1 z1) * ( Im2 z))) - (( Im2 z1) * ( Im1 z))) * <k> )) by QUATERNI: 93

 .= [*( - ( Im2 z1)), ( - ( Im3 z1)), ( Rea z1), ( Im1 z1)*] by QUATERN2: 1, QUATERNI: 31;

 then

 A4: ( Rea (z1 * z)) = ( - ( Im2 z1)) & ( Im1 (z1 * z)) = ( - ( Im3 z1)) by QUATERNI: 23;



 A5: ( Im2 (z1 * z)) = ( Rea z1) & ( Im3 (z1 * z)) = ( Im1 z1) by A3, QUATERNI: 23;

 ( Rea (z * z1)) = ( - ( Im2 z1)) & ( Im1 (z * z1)) = ( Im3 z1) by A1, QUATERNI: 23;

 then ((z1 * z) + (z * z1)) = ((((( - ( Im2 z1)) + ( - ( Im2 z1))) + ((( Im3 z1) - ( Im3 z1)) * )) + ((( Rea z1) + ( Rea z1)) * <j> )) + ((( - ( Im1 z1)) + ( Im1 z1)) * <k> )) by A2, A4, A5, QUATERNI: 92;

 hence thesis by QUATERN2: 1;

 end;

 theorem :: QUATERN3:22

 (( <k> * z1) - (z1 * <k> )) = [* 0 , ( - (2 * ( Im2 z1))), (2 * ( Im1 z1)), 0 *]

 proof

 set z = <k> ;



 A1: (z * z1) = (((((((( Rea z) * ( Rea z1)) - (( Im1 z) * ( Im1 z1))) - (( Im2 z) * ( Im2 z1))) - (( Im3 z) * ( Im3 z1))) + (((((( Rea z) * ( Im1 z1)) + (( Im1 z) * ( Rea z1))) + (( Im2 z) * ( Im3 z1))) - (( Im3 z) * ( Im2 z1))) * )) + (((((( Rea z) * ( Im2 z1)) + (( Im2 z) * ( Rea z1))) + (( Im3 z) * ( Im1 z1))) - (( Im1 z) * ( Im3 z1))) * <j> )) + (((((( Rea z) * ( Im3 z1)) + (( Im3 z) * ( Rea z1))) + (( Im1 z) * ( Im2 z1))) - (( Im2 z) * ( Im1 z1))) * <k> )) by QUATERNI: 93

 .= [*( - ( Im3 z1)), ( - ( Im2 z1)), ( Im1 z1), ( Rea z1)*] by QUATERN2: 1, QUATERNI: 31;

 (z1 * z) = (((((((( Rea z1) * ( Rea z)) - (( Im1 z1) * ( Im1 z))) - (( Im2 z1) * ( Im2 z))) - (( Im3 z1) * ( Im3 z))) + (((((( Rea z1) * ( Im1 z)) + (( Im1 z1) * ( Rea z))) + (( Im2 z1) * ( Im3 z))) - (( Im3 z1) * ( Im2 z))) * )) + (((((( Rea z1) * ( Im2 z)) + (( Im2 z1) * ( Rea z))) + (( Im3 z1) * ( Im1 z))) - (( Im1 z1) * ( Im3 z))) * <j> )) + (((((( Rea z1) * ( Im3 z)) + (( Im3 z1) * ( Rea z))) + (( Im1 z1) * ( Im2 z))) - (( Im2 z1) * ( Im1 z))) * <k> )) by QUATERNI: 93

 .= [*( - ( Im3 z1)), ( Im2 z1), ( - ( Im1 z1)), ( Rea z1)*] by QUATERN2: 1, QUATERNI: 31;



 then ((z * z1) - (z1 * z)) = [*(( - ( Im3 z1)) - ( - ( Im3 z1))), (( - ( Im2 z1)) - ( Im2 z1)), (( Im1 z1) - ( - ( Im1 z1))), (( Rea z1) - ( Rea z1))*] by A1, QUATERN2: 5

 .= [* 0 , ( - (2 * ( Im2 z1))), (2 * ( Im1 z1)), 0 *];

 hence thesis;

 end;

 theorem :: QUATERN3:23

 (( <k> * z1) + (z1 * <k> )) = [*( - (2 * ( Im3 z1))), 0 , 0 , (2 * ( Rea z1))*]

 proof

 set z = <k> ;



 A1: (z * z1) = (((((((( Rea z) * ( Rea z1)) - (( Im1 z) * ( Im1 z1))) - (( Im2 z) * ( Im2 z1))) - (( Im3 z) * ( Im3 z1))) + (((((( Rea z) * ( Im1 z1)) + (( Im1 z) * ( Rea z1))) + (( Im2 z) * ( Im3 z1))) - (( Im3 z) * ( Im2 z1))) * )) + (((((( Rea z) * ( Im2 z1)) + (( Im2 z) * ( Rea z1))) + (( Im3 z) * ( Im1 z1))) - (( Im1 z) * ( Im3 z1))) * <j> )) + (((((( Rea z) * ( Im3 z1)) + (( Im3 z) * ( Rea z1))) + (( Im1 z) * ( Im2 z1))) - (( Im2 z) * ( Im1 z1))) * <k> )) by QUATERNI: 93

 .= [*( - ( Im3 z1)), ( - ( Im2 z1)), ( Im1 z1), ( Rea z1)*] by QUATERN2: 1, QUATERNI: 31;

 then

 A2: ( Im2 (z * z1)) = ( Im1 z1) & ( Im3 (z * z1)) = ( Rea z1) by QUATERNI: 23;



 A3: (z1 * z) = (((((((( Rea z1) * ( Rea z)) - (( Im1 z1) * ( Im1 z))) - (( Im2 z1) * ( Im2 z))) - (( Im3 z1) * ( Im3 z))) + (((((( Rea z1) * ( Im1 z)) + (( Im1 z1) * ( Rea z))) + (( Im2 z1) * ( Im3 z))) - (( Im3 z1) * ( Im2 z))) * )) + (((((( Rea z1) * ( Im2 z)) + (( Im2 z1) * ( Rea z))) + (( Im3 z1) * ( Im1 z))) - (( Im1 z1) * ( Im3 z))) * <j> )) + (((((( Rea z1) * ( Im3 z)) + (( Im3 z1) * ( Rea z))) + (( Im1 z1) * ( Im2 z))) - (( Im2 z1) * ( Im1 z))) * <k> )) by QUATERNI: 93

 .= [*( - ( Im3 z1)), ( Im2 z1), ( - ( Im1 z1)), ( Rea z1)*] by QUATERN2: 1, QUATERNI: 31;

 then

 A4: ( Rea (z1 * z)) = ( - ( Im3 z1)) & ( Im1 (z1 * z)) = ( Im2 z1) by QUATERNI: 23;



 A5: ( Im2 (z1 * z)) = ( - ( Im1 z1)) & ( Im3 (z1 * z)) = ( Rea z1) by A3, QUATERNI: 23;

 ( Rea (z * z1)) = ( - ( Im3 z1)) & ( Im1 (z * z1)) = ( - ( Im2 z1)) by A1, QUATERNI: 23;

 then ((z1 * z) + (z * z1)) = ((((( - ( Im3 z1)) + ( - ( Im3 z1))) + ((( - ( Im2 z1)) + ( Im2 z1)) * )) + ((( Im1 z1) - ( Im1 z1)) * <j> )) + ((( Rea z1) + ( Rea z1)) * <k> )) by A2, A4, A5, QUATERNI: 92;

 hence thesis by QUATERN2: 1;

 end;

 theorem :: QUATERN3:24



 Th24: ( Rea ((1 / ( |.z.| ^2 )) * (z *' ))) = ((1 / ( |.z.| ^2 )) * ( Rea z))

 proof

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

 then ((1 / ( |.z.| ^2 )) * (z *' )) = [*((1 / ( |.z.| ^2 )) * ( Rea z)), ((1 / ( |.z.| ^2 )) * ( - ( Im1 z))), ((1 / ( |.z.| ^2 )) * ( - ( Im2 z))), ((1 / ( |.z.| ^2 )) * ( - ( Im3 z)))*] by QUATERNI:def 21;

 hence thesis by QUATERNI: 23;

 end;

 theorem :: QUATERN3:25



 Th25: ( Im1 ((1 / ( |.z.| ^2 )) * (z *' ))) = ( - ((1 / ( |.z.| ^2 )) * ( Im1 z)))

 proof

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

 then ((1 / ( |.z.| ^2 )) * (z *' )) = [*((1 / ( |.z.| ^2 )) * ( Rea z)), ((1 / ( |.z.| ^2 )) * ( - ( Im1 z))), ((1 / ( |.z.| ^2 )) * ( - ( Im2 z))), ((1 / ( |.z.| ^2 )) * ( - ( Im3 z)))*] by QUATERNI:def 21;

 hence thesis by QUATERNI: 23;

 end;

 theorem :: QUATERN3:26



 Th26: ( Im2 ((1 / ( |.z.| ^2 )) * (z *' ))) = ( - ((1 / ( |.z.| ^2 )) * ( Im2 z)))

 proof

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

 then ((1 / ( |.z.| ^2 )) * (z *' )) = [*((1 / ( |.z.| ^2 )) * ( Rea z)), ((1 / ( |.z.| ^2 )) * ( - ( Im1 z))), ((1 / ( |.z.| ^2 )) * ( - ( Im2 z))), ((1 / ( |.z.| ^2 )) * ( - ( Im3 z)))*] by QUATERNI:def 21;

 hence thesis by QUATERNI: 23;

 end;

 theorem :: QUATERN3:27



 Th27: ( Im3 ((1 / ( |.z.| ^2 )) * (z *' ))) = ( - ((1 / ( |.z.| ^2 )) * ( Im3 z)))

 proof

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

 then ((1 / ( |.z.| ^2 )) * (z *' )) = [*((1 / ( |.z.| ^2 )) * ( Rea z)), ((1 / ( |.z.| ^2 )) * ( - ( Im1 z))), ((1 / ( |.z.| ^2 )) * ( - ( Im2 z))), ((1 / ( |.z.| ^2 )) * ( - ( Im3 z)))*] by QUATERNI:def 21;

 hence thesis by QUATERNI: 23;

 end;

 theorem :: QUATERN3:28

 ((1 / ( |.z.| ^2 )) * (z *' )) = [*((1 / ( |.z.| ^2 )) * ( Rea z)), ( - ((1 / ( |.z.| ^2 )) * ( Im1 z))), ( - ((1 / ( |.z.| ^2 )) * ( Im2 z))), ( - ((1 / ( |.z.| ^2 )) * ( Im3 z)))*]

 proof

 set zz = ( |.z.| ^2 );

 ((1 / zz) * (z *' )) = [*( Rea ((1 / zz) * (z *' ))), ( Im1 ((1 / zz) * (z *' ))), ( Im2 ((1 / zz) * (z *' ))), ( Im3 ((1 / zz) * (z *' )))*] by QUATERNI: 24;

 then ((1 / zz) * (z *' )) = [*((1 / zz) * ( Rea z)), ( Im1 ((1 / zz) * (z *' ))), ( Im2 ((1 / zz) * (z *' ))), ( Im3 ((1 / zz) * (z *' )))*] by Th24;

 then ((1 / zz) * (z *' )) = [*((1 / zz) * ( Rea z)), ( - ((1 / zz) * ( Im1 z))), ( Im2 ((1 / zz) * (z *' ))), ( Im3 ((1 / zz) * (z *' )))*] by Th25;

 then ((1 / zz) * (z *' )) = [*((1 / zz) * ( Rea z)), ( - ((1 / zz) * ( Im1 z))), ( - ((1 / zz) * ( Im2 z))), ( Im3 ((1 / zz) * (z *' )))*] by Th26;

 hence thesis by Th27;

 end;

 theorem :: QUATERN3:29

 (z * ((1 / ( |.z.| ^2 )) * (z *' ))) = [*(( |.z.| ^2 ) / ( |.z.| ^2 )), 0 , 0 , 0 *]

 proof

 set zz = ( |.z.| ^2 );

 set z3 = ((1 / zz) * (z *' ));

 (z * ((1 / zz) * (z *' ))) = (((((((( Rea z) * ( Rea z3)) - (( Im1 z) * ( Im1 z3))) - (( Im2 z) * ( Im2 z3))) - (( Im3 z) * ( Im3 z3))) + (((((( Rea z) * ( Im1 z3)) + (( Im1 z) * ( Rea z3))) + (( Im2 z) * ( Im3 z3))) - (( Im3 z) * ( Im2 z3))) * )) + (((((( Rea z) * ( Im2 z3)) + (( Im2 z) * ( Rea z3))) + (( Im3 z) * ( Im1 z3))) - (( Im1 z) * ( Im3 z3))) * <j> )) + (((((( Rea z) * ( Im3 z3)) + (( Im3 z) * ( Rea z3))) + (( Im1 z) * ( Im2 z3))) - (( Im2 z) * ( Im1 z3))) * <k> )) by QUATERNI: 93

 .= [*((((( Rea z) * ( Rea z3)) - (( Im1 z) * ( Im1 z3))) - (( Im2 z) * ( Im2 z3))) - (( Im3 z) * ( Im3 z3))), ((((( Rea z) * ( Im1 z3)) + (( Im1 z) * ( Rea z3))) + (( Im2 z) * ( Im3 z3))) - (( Im3 z) * ( Im2 z3))), ((((( Rea z) * ( Im2 z3)) + (( Im2 z) * ( Rea z3))) + (( Im3 z) * ( Im1 z3))) - (( Im1 z) * ( Im3 z3))), ((((( Rea z) * ( Im3 z3)) + (( Im3 z) * ( Rea z3))) + (( Im1 z) * ( Im2 z3))) - (( Im2 z) * ( Im1 z3)))*] by QUATERN2: 1

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( Im1 z3))) - (( Im2 z) * ( Im2 z3))) - (( Im3 z) * ( Im3 z3))), ((((( Rea z) * ( Im1 z3)) + (( Im1 z) * ( Rea z3))) + (( Im2 z) * ( Im3 z3))) - (( Im3 z) * ( Im2 z3))), ((((( Rea z) * ( Im2 z3)) + (( Im2 z) * ( Rea z3))) + (( Im3 z) * ( Im1 z3))) - (( Im1 z) * ( Im3 z3))), ((((( Rea z) * ( Im3 z3)) + (( Im3 z) * ( Rea z3))) + (( Im1 z) * ( Im2 z3))) - (( Im2 z) * ( Im1 z3)))*] by Th24

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( Im2 z3))) - (( Im3 z) * ( Im3 z3))), ((((( Rea z) * ( Im1 z3)) + (( Im1 z) * ( Rea z3))) + (( Im2 z) * ( Im3 z3))) - (( Im3 z) * ( Im2 z3))), ((((( Rea z) * ( Im2 z3)) + (( Im2 z) * ( Rea z3))) + (( Im3 z) * ( Im1 z3))) - (( Im1 z) * ( Im3 z3))), ((((( Rea z) * ( Im3 z3)) + (( Im3 z) * ( Rea z3))) + (( Im1 z) * ( Im2 z3))) - (( Im2 z) * ( Im1 z3)))*] by Th25

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im3 z) * ( Im3 z3))), ((((( Rea z) * ( Im1 z3)) + (( Im1 z) * ( Rea z3))) + (( Im2 z) * ( Im3 z3))) - (( Im3 z) * ( Im2 z3))), ((((( Rea z) * ( Im2 z3)) + (( Im2 z) * ( Rea z3))) + (( Im3 z) * ( Im1 z3))) - (( Im1 z) * ( Im3 z3))), ((((( Rea z) * ( Im3 z3)) + (( Im3 z) * ( Rea z3))) + (( Im1 z) * ( Im2 z3))) - (( Im2 z) * ( Im1 z3)))*] by Th26

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( Im1 z3)) + (( Im1 z) * ( Rea z3))) + (( Im2 z) * ( Im3 z3))) - (( Im3 z) * ( Im2 z3))), ((((( Rea z) * ( Im2 z3)) + (( Im2 z) * ( Rea z3))) + (( Im3 z) * ( Im1 z3))) - (( Im1 z) * ( Im3 z3))), ((((( Rea z) * ( Im3 z3)) + (( Im3 z) * ( Rea z3))) + (( Im1 z) * ( Im2 z3))) - (( Im2 z) * ( Im1 z3)))*] by Th27

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im1 z)))) + (( Im1 z) * ( Rea ((1 / zz) * (z *' ))))) + (( Im2 z) * ( Im3 ((1 / zz) * (z *' ))))) - (( Im3 z) * ( Im2 ((1 / zz) * (z *' ))))), ((((( Rea z) * ( Im2 ((1 / zz) * (z *' )))) + (( Im2 z) * ( Rea ((1 / zz) * (z *' ))))) + (( Im3 z) * ( Im1 ((1 / zz) * (z *' ))))) - (( Im1 z) * ( Im3 ((1 / zz) * (z *' ))))), ((((( Rea z) * ( Im3 ((1 / zz) * (z *' )))) + (( Im3 z) * ( Rea ((1 / zz) * (z *' ))))) + (( Im1 z) * ( Im2 ((1 / zz) * (z *' ))))) - (( Im2 z) * ( Im1 ((1 / zz) * (z *' )))))*] by Th25

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im1 z)))) + (( Im1 z) * ((1 / zz) * ( Rea z)))) + (( Im2 z) * ( Im3 ((1 / zz) * (z *' ))))) - (( Im3 z) * ( Im2 ((1 / zz) * (z *' ))))), ((((( Rea z) * ( Im2 ((1 / zz) * (z *' )))) + (( Im2 z) * ( Rea ((1 / zz) * (z *' ))))) + (( Im3 z) * ( Im1 ((1 / zz) * (z *' ))))) - (( Im1 z) * ( Im3 ((1 / zz) * (z *' ))))), ((((( Rea z) * ( Im3 ((1 / zz) * (z *' )))) + (( Im3 z) * ( Rea ((1 / zz) * (z *' ))))) + (( Im1 z) * ( Im2 ((1 / zz) * (z *' ))))) - (( Im2 z) * ( Im1 ((1 / zz) * (z *' )))))*] by Th24

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im1 z)))) + (( Im1 z) * ((1 / zz) * ( Rea z)))) + (( Im2 z) * ( - ((1 / zz) * ( Im3 z))))) - (( Im3 z) * ( Im2 z3))), ((((( Rea z) * ( Im2 z3)) + (( Im2 z) * ( Rea z3))) + (( Im3 z) * ( Im1 z3))) - (( Im1 z) * ( Im3 z3))), ((((( Rea z) * ( Im3 z3)) + (( Im3 z) * ( Rea z3))) + (( Im1 z) * ( Im2 z3))) - (( Im2 z) * ( Im1 z3)))*] by Th27

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im1 z)))) + (( Im1 z) * ((1 / zz) * ( Rea z)))) + (( Im2 z) * ( - ((1 / zz) * ( Im3 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im2 z))))), ((((( Rea z) * ( Im2 z3)) + (( Im2 z) * ( Rea z3))) + (( Im3 z) * ( Im1 z3))) - (( Im1 z) * ( Im3 z3))), ((((( Rea z) * ( Im3 z3)) + (( Im3 z) * ( Rea z3))) + (( Im1 z) * ( Im2 z3))) - (( Im2 z) * ( Im1 z3)))*] by Th26

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im1 z)))) + (( Im1 z) * ((1 / zz) * ( Rea z)))) + (( Im2 z) * ( - ((1 / zz) * ( Im3 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im2 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im2 z)))) + (( Im2 z) * ( Rea z3))) + (( Im3 z) * ( Im1 z3))) - (( Im1 z) * ( Im3 z3))), ((((( Rea z) * ( Im3 z3)) + (( Im3 z) * ( Rea z3))) + (( Im1 z) * ( Im2 z3))) - (( Im2 z) * ( Im1 z3)))*] by Th26

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im1 z)))) + (( Im1 z) * ((1 / zz) * ( Rea z)))) + (( Im2 z) * ( - ((1 / zz) * ( Im3 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im2 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im2 z)))) + (( Im2 z) * ((1 / zz) * ( Rea z)))) + (( Im3 z) * ( Im1 z3))) - (( Im1 z) * ( Im3 z3))), ((((( Rea z) * ( Im3 z3)) + (( Im3 z) * ( Rea z3))) + (( Im1 z) * ( Im2 z3))) - (( Im2 z) * ( Im1 ((1 / zz) * (z *' )))))*] by Th24

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im1 z)))) + (( Im1 z) * ((1 / zz) * ( Rea z)))) + (( Im2 z) * ( - ((1 / zz) * ( Im3 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im2 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im2 z)))) + (( Im2 z) * ((1 / zz) * ( Rea z)))) + (( Im3 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im1 z) * ( Im3 z3))), ((((( Rea z) * ( Im3 z3)) + (( Im3 z) * ( Rea z3))) + (( Im1 z) * ( Im2 z3))) - (( Im2 z) * ( Im1 z3)))*] by Th25

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im1 z)))) + (( Im1 z) * ((1 / zz) * ( Rea z)))) + (( Im2 z) * ( - ((1 / zz) * ( Im3 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im2 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im2 z)))) + (( Im2 z) * ((1 / zz) * ( Rea z)))) + (( Im3 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im1 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( Im3 ((1 / zz) * (z *' )))) + (( Im3 z) * ( Rea z3))) + (( Im1 z) * ( Im2 z3))) - (( Im2 z) * ( Im1 z3)))*] by Th27

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im1 z)))) + (( Im1 z) * ((1 / zz) * ( Rea z)))) + (( Im2 z) * ( - ((1 / zz) * ( Im3 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im2 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im2 z)))) + (( Im2 z) * ((1 / zz) * ( Rea z)))) + (( Im3 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im1 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im3 z)))) + (( Im3 z) * ( Rea ((1 / zz) * (z *' ))))) + (( Im1 z) * ( Im2 ((1 / zz) * (z *' ))))) - (( Im2 z) * ( Im1 ((1 / zz) * (z *' )))))*] by Th27

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im1 z)))) + (( Im1 z) * ((1 / zz) * ( Rea z)))) + (( Im2 z) * ( - ((1 / zz) * ( Im3 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im2 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im2 z)))) + (( Im2 z) * ((1 / zz) * ( Rea z)))) + (( Im3 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im1 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im3 z)))) + (( Im3 z) * ((1 / zz) * ( Rea z)))) + (( Im1 z) * ( Im2 ((1 / zz) * (z *' ))))) - (( Im2 z) * ( Im1 ((1 / zz) * (z *' )))))*] by Th24

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im1 z)))) + (( Im1 z) * ((1 / zz) * ( Rea z)))) + (( Im2 z) * ( - ((1 / zz) * ( Im3 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im2 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im2 z)))) + (( Im2 z) * ((1 / zz) * ( Rea z)))) + (( Im3 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im1 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im3 z)))) + (( Im3 z) * ((1 / zz) * ( Rea z)))) + (( Im1 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im2 z) * ( Im1 ((1 / zz) * (z *' )))))*] by Th26

 .= [*((((( Rea z) * ((1 / zz) * ( Rea z))) - (( Im1 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im1 z)))) + (( Im1 z) * ((1 / zz) * ( Rea z)))) + (( Im2 z) * ( - ((1 / zz) * ( Im3 z))))) - (( Im3 z) * ( - ((1 / zz) * ( Im2 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im2 z)))) + (( Im2 z) * ((1 / zz) * ( Rea z)))) + (( Im3 z) * ( - ((1 / zz) * ( Im1 z))))) - (( Im1 z) * ( - ((1 / zz) * ( Im3 z))))), ((((( Rea z) * ( - ((1 / zz) * ( Im3 z)))) + (( Im3 z) * ((1 / zz) * ( Rea z)))) + (( Im1 z) * ( - ((1 / zz) * ( Im2 z))))) - (( Im2 z) * ( - ((1 / zz) * ( Im1 z)))))*] by Th25

 .= [*(((((( Rea z) ^2 ) + (( Im1 z) ^2 )) + (( Im2 z) ^2 )) + (( Im3 z) ^2 )) / zz), 0 , 0 , 0 *]

 .= [*(zz / zz), 0 , 0 , 0 *] by Th11;

 hence thesis;

 end;

 theorem :: QUATERN3:30

 ( |.((z1 * z2) * z3).| ^2 ) = ((( |.z1.| ^2 ) * ( |.z2.| ^2 )) * ( |.z3.| ^2 ))

 proof

 ( |.((z1 * z2) * z3).| ^2 ) = ( |.(z1 * (z2 * z3)).| ^2 ) by QUATERN2: 16

 .= (( |.z1.| ^2 ) * ( |.(z2 * z3).| ^2 )) by Th17

 .= (( |.z1.| ^2 ) * (( |.z2.| ^2 ) * ( |.z3.| ^2 ))) by Th17

 .= ((( |.z1.| ^2 ) * ( |.z2.| ^2 )) * ( |.z3.| ^2 ));

 hence thesis;

 end;

 theorem :: QUATERN3:31

 ( Rea ((z1 * z2) * z3)) = ( Rea ((z3 * z1) * z2))

 proof

 ( Rea ((z1 * z2) * z3)) = ( Rea (z1 * (z2 * z3))) by QUATERN2: 16

 .= ( Rea ((z2 * z3) * z1)) by Th1

 .= ( Rea (z2 * (z3 * z1))) by QUATERN2: 16

 .= ( Rea ((z3 * z1) * z2)) by Th1;

 hence thesis;

 end;

 theorem :: QUATERN3:32



 Th32: |.(z * z).| = |.((z *' ) * (z *' )).|

 proof

 |.((z *' ) * (z *' )).| = ( |.(z *' ).| * |.(z *' ).|) by QUATERNI: 87

 .= ( |.z.| * |.(z *' ).|) by QUATERNI: 73

 .= ( |.z.| * |.z.|) by QUATERNI: 73;

 hence thesis by QUATERNI: 87;

 end;

 theorem :: QUATERN3:33

 |.((z *' ) * (z *' )).| = ( |.z.| ^2 )

 proof

 |.((z *' ) * (z *' )).| = |.(z * z).| by Th32;

 hence thesis by QUATERNI: 87;

 end;

 theorem :: QUATERN3:34

 |.((z1 * z2) * z3).| = (( |.z1.| * |.z2.|) * |.z3.|)

 proof

 |.((z1 * z2) * z3).| = |.(z1 * (z2 * z3)).| by QUATERN2: 16

 .= ( |.z1.| * |.(z2 * z3).|) by QUATERNI: 87

 .= ( |.z1.| * ( |.z2.| * |.z3.|)) by QUATERNI: 87

 .= (( |.z1.| * |.z2.|) * |.z3.|);

 hence thesis;

 end;

 theorem :: QUATERN3:35

 |.((z1 + z2) + z3).| <= (( |.z1.| + |.z2.|) + |.z3.|)

 proof

 |.((z1 + z2) + z3).| = |.(z1 + (z2 + z3)).| by QUATERN2: 2;

 then |.((z1 + z2) + z3).| <= ( |.z1.| + |.(z2 + z3).|) by QUATERNI: 79;

 then

 A1: ( |.((z1 + z2) + z3).| - |.z1.|) <= |.(z2 + z3).| by XREAL_1: 20;

 |.(z2 + z3).| <= ( |.z2.| + |.z3.|) by QUATERNI: 79;

 then (( |.((z1 + z2) + z3).| - |.z1.|) + |.(z2 + z3).|) <= ( |.(z2 + z3).| + ( |.z2.| + |.z3.|)) by A1, XREAL_1: 7;

 then ( |.((z1 + z2) + z3).| - |.z1.|) <= (( |.(z2 + z3).| + ( |.z2.| + |.z3.|)) - |.(z2 + z3).|) by XREAL_1: 19;

 then |.((z1 + z2) + z3).| <= (( |.z2.| + |.z3.|) + |.z1.|) by XREAL_1: 20;

 hence thesis;

 end;

 theorem :: QUATERN3:36

 |.((z1 + z2) - z3).| <= (( |.z1.| + |.z2.|) + |.z3.|)

 proof

 |.((z1 + z2) - z3).| = |.(z1 + (z2 - z3)).| by QUATERN2: 2;

 then |.((z1 + z2) - z3).| <= ( |.z1.| + |.(z2 - z3).|) by QUATERNI: 79;

 then

 A1: ( |.((z1 + z2) - z3).| - |.z1.|) <= |.(z2 - z3).| by XREAL_1: 20;

 |.(z2 - z3).| <= ( |.z2.| + |.z3.|) by QUATERNI: 80;

 then (( |.((z1 + z2) - z3).| - |.z1.|) + |.(z2 - z3).|) <= ( |.(z2 - z3).| + ( |.z2.| + |.z3.|)) by A1, XREAL_1: 7;

 then ( |.((z1 + z2) - z3).| - |.z1.|) <= (( |.(z2 - z3).| + ( |.z2.| + |.z3.|)) - |.(z2 - z3).|) by XREAL_1: 19;

 then |.((z1 + z2) - z3).| <= (( |.z2.| + |.z3.|) + |.z1.|) by XREAL_1: 20;

 hence thesis;

 end;

 theorem :: QUATERN3:37

 |.((z1 - z2) - z3).| <= (( |.z1.| + |.z2.|) + |.z3.|)

 proof

 |.((z1 - z2) - z3).| <= ( |.(z1 - z2).| + |.z3.|) & |.(z1 - z2).| <= ( |.z1.| + |.z2.|) by QUATERNI: 80;

 then ( |.((z1 - z2) - z3).| + |.(z1 - z2).|) <= (( |.(z1 - z2).| + |.z3.|) + ( |.z1.| + |.z2.|)) by XREAL_1: 7;

 then |.((z1 - z2) - z3).| <= ((( |.(z1 - z2).| + |.z3.|) + ( |.z1.| + |.z2.|)) - |.(z1 - z2).|) by XREAL_1: 19;

 hence thesis;

 end;

 theorem :: QUATERN3:38

 ( |.z1.| - |.z2.|) <= (( |.(z1 + z2).| + |.(z1 - z2).|) / 2)

 proof

 ( |.z1.| - |.z2.|) <= |.(z1 + z2).| & ( |.z1.| - |.z2.|) <= |.(z1 - z2).| by QUATERNI: 81, QUATERNI: 82;

 then (( |.z1.| - |.z2.|) + ( |.z1.| - |.z2.|)) <= ( |.(z1 + z2).| + |.(z1 - z2).|) by XREAL_1: 7;

 then (2 * ( |.z1.| - |.z2.|)) <= ( |.(z1 + z2).| + |.(z1 - z2).|);

 hence thesis by XREAL_1: 77;

 end;

 theorem :: QUATERN3:39

 ( |.z1.| - |.z2.|) <= (( |.(z1 + z2).| + |.(z2 - z1).|) / 2)

 proof

 ( |.z1.| - |.z2.|) <= |.(z1 + z2).| & ( |.z1.| - |.z2.|) <= |.(z1 - z2).| by QUATERNI: 81, QUATERNI: 82;

 then (( |.z1.| - |.z2.|) + ( |.z1.| - |.z2.|)) <= ( |.(z1 + z2).| + |.(z1 - z2).|) by XREAL_1: 7;

 then (2 * ( |.z1.| - |.z2.|)) <= ( |.(z1 + z2).| + |.(z2 - z1).|) by QUATERNI: 83;

 hence thesis by XREAL_1: 77;

 end;

 theorem :: QUATERN3:40

 |.( |.z1.| - |.z2.|).| <= |.(z2 - z1).|

 proof

 |.( |.z1.| - |.z2.|).| <= |.(z1 - z2).| by QUATERNI: 86;

 hence thesis by QUATERNI: 83;

 end;

 theorem :: QUATERN3:41

 |.( |.z1.| - |.z2.|).| <= ( |.z1.| + |.z2.|)

 proof

 |.( |.z1.| - |.z2.|).| <= |.(z1 - z2).| & |.(z1 - z2).| <= ( |.z1.| + |.z2.|) by QUATERNI: 80, QUATERNI: 86;

 then ( |.( |.z1.| - |.z2.|).| + |.(z1 - z2).|) <= ( |.(z1 - z2).| + ( |.z1.| + |.z2.|)) by XREAL_1: 7;

 then |.( |.z1.| - |.z2.|).| <= ((( |.(z1 - z2).| + |.z1.|) + |.z2.|) - |.(z1 - z2).|) by XREAL_1: 19;

 hence thesis;

 end;

 theorem :: QUATERN3:42

 ( |.z1.| - |.z2.|) <= ( |.(z1 - z).| + |.(z - z2).|)

 proof

 ( |.z1.| - |.z2.|) <= |.(z1 - z2).| & |.(z1 - z2).| <= ( |.(z1 - z).| + |.(z - z2).|) by QUATERNI: 82, QUATERNI: 85;

 then (( |.z1.| - |.z2.|) + |.(z1 - z2).|) <= ( |.(z1 - z2).| + ( |.(z1 - z).| + |.(z - z2).|)) by XREAL_1: 7;

 then ( |.z1.| - |.z2.|) <= ((( |.(z1 - z2).| + |.(z1 - z).|) + |.(z - z2).|) - |.(z1 - z2).|) by XREAL_1: 19;

 hence thesis;

 end;

 theorem :: QUATERN3:43

 ( |.z1.| - |.z2.|) <> 0 implies ((( |.z1.| ^2 ) + ( |.z2.| ^2 )) - ((2 * |.z1.|) * |.z2.|)) > 0

 proof

 assume ( |.z1.| - |.z2.|) <> 0 ;

 then (( |.z1.| - |.z2.|) ^2 ) > 0 by SQUARE_1: 12;

 hence thesis;

 end;

 theorem :: QUATERN3:44

 ( |.z1.| + |.z2.|) >= (( |.(z1 + z2).| + |.(z2 - z1).|) / 2)

 proof

 |.(z1 + z2).| <= ( |.z1.| + |.z2.|) & |.(z1 - z2).| <= ( |.z1.| + |.z2.|) by QUATERNI: 79, QUATERNI: 80;

 then ( |.(z1 + z2).| + |.(z1 - z2).|) <= (( |.z1.| + |.z2.|) + ( |.z1.| + |.z2.|)) by XREAL_1: 7;

 then ( |.(z1 + z2).| + |.(z2 - z1).|) <= (2 * ( |.z1.| + |.z2.|)) by QUATERNI: 83;

 hence thesis by XREAL_1: 79;

 end;

 theorem :: QUATERN3:45

 ( |.z1.| + |.z2.|) >= (( |.(z1 + z2).| + |.(z1 - z2).|) / 2)

 proof

 |.(z1 + z2).| <= ( |.z1.| + |.z2.|) & |.(z1 - z2).| <= ( |.z1.| + |.z2.|) by QUATERNI: 79, QUATERNI: 80;

 then ( |.(z1 + z2).| + |.(z1 - z2).|) <= (( |.z1.| + |.z2.|) + ( |.z1.| + |.z2.|)) by XREAL_1: 7;

 then ( |.(z1 + z2).| + |.(z1 - z2).|) <= (2 * ( |.z1.| + |.z2.|));

 hence thesis by XREAL_1: 79;

 end;

 theorem :: QUATERN3:46

 ((z1 * z2) " ) = ((z2 " ) * (z1 " ))

 proof

 set z3 = (z1 * z2);



 A1: ((((( Rea (z2 " )) * ( Im1 (z1 " ))) + (( Im1 (z2 " )) * ( Rea (z1 " )))) + (( Im2 (z2 " )) * ( Im3 (z1 " )))) - (( Im3 (z2 " )) * ( Im2 (z1 " )))) = (((((( Rea z2) / ( |.z2.| ^2 )) * ( Im1 (z1 " ))) + (( Im1 (z2 " )) * ( Rea (z1 " )))) + (( Im2 (z2 " )) * ( Im3 (z1 " )))) - (( Im3 (z2 " )) * ( Im2 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im1 z1) / ( |.z1.| ^2 )))) + (( Im1 (z2 " )) * ( Rea (z1 " )))) + (( Im2 (z2 " )) * ( Im3 (z1 " )))) - (( Im3 (z2 " )) * ( Im2 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im1 z1) / ( |.z1.| ^2 )))) + (( - (( Im1 z2) / ( |.z2.| ^2 ))) * ( Rea (z1 " )))) + (( Im2 (z2 " )) * ( Im3 (z1 " )))) - (( Im3 (z2 " )) * ( Im2 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im1 z1) / ( |.z1.| ^2 )))) + (( - (( Im1 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( Im2 (z2 " )) * ( Im3 (z1 " )))) - (( Im3 (z2 " )) * ( Im2 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im1 z1) / ( |.z1.| ^2 )))) + (( - (( Im1 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( - (( Im2 z2) / ( |.z2.| ^2 ))) * ( Im3 (z1 " )))) - (( Im3 (z2 " )) * ( Im2 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im1 z1) / ( |.z1.| ^2 )))) + (( - (( Im1 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( - (( Im2 z2) / ( |.z2.| ^2 ))) * ( - (( Im3 z1) / ( |.z1.| ^2 ))))) - (( Im3 (z2 " )) * ( Im2 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im1 z1) / ( |.z1.| ^2 )))) + (( - (( Im1 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( - (( Im2 z2) / ( |.z2.| ^2 ))) * ( - (( Im3 z1) / ( |.z1.| ^2 ))))) - (( - (( Im3 z2) / ( |.z2.| ^2 ))) * ( Im2 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * (( - ( Im1 z1)) / ( |.z1.| ^2 ))) + (( - (( Im1 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( - (( Im2 z2) / ( |.z2.| ^2 ))) * ( - (( Im3 z1) / ( |.z1.| ^2 ))))) - (( - (( Im3 z2) / ( |.z2.| ^2 ))) * ( - (( Im2 z1) / ( |.z1.| ^2 ))))) by QUATERN2: 29

 .= (((((( Rea z2) * ( - ( Im1 z1))) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) + ((( - ( Im1 z2)) / ( |.z2.| ^2 )) * (( Rea z1) / ( |.z1.| ^2 )))) + (( - (( Im2 z2) / ( |.z2.| ^2 ))) * ( - (( Im3 z1) / ( |.z1.| ^2 ))))) - (( - (( Im3 z2) / ( |.z2.| ^2 ))) * ( - (( Im2 z1) / ( |.z1.| ^2 ))))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( - ( Im1 z1))) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) + ((( - ( Im1 z2)) * ( Rea z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) + ((( Im2 z2) / ( |.z2.| ^2 )) * (( Im3 z1) / ( |.z1.| ^2 )))) - (( - (( Im3 z2) / ( |.z2.| ^2 ))) * ( - (( Im2 z1) / ( |.z1.| ^2 ))))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( - ( Im1 z1))) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) + ((( - ( Im1 z2)) * ( Rea z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) + ((( Im2 z2) * ( Im3 z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) - ((( Im3 z2) / ( |.z2.| ^2 )) * (( Im2 z1) / ( |.z1.| ^2 )))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( - ( Im1 z1))) + (( - ( Im1 z2)) * ( Rea z1))) + (( Im2 z2) * ( Im3 z1))) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) - ((( Im3 z2) * ( Im2 z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( - ( Im1 z1))) + (( - ( Im1 z2)) * ( Rea z1))) + (( Im2 z2) * ( Im3 z1))) - (( Im3 z2) * ( Im2 z1))) / (( |.z2.| * |.z1.|) ^2 ));



 A2: ((((( Rea (z2 " )) * ( Im2 (z1 " ))) + (( Im2 (z2 " )) * ( Rea (z1 " )))) + (( Im3 (z2 " )) * ( Im1 (z1 " )))) - (( Im1 (z2 " )) * ( Im3 (z1 " )))) = (((((( Rea z2) / ( |.z2.| ^2 )) * ( Im2 (z1 " ))) + (( Im2 (z2 " )) * ( Rea (z1 " )))) + (( Im3 (z2 " )) * ( Im1 (z1 " )))) - (( Im1 (z2 " )) * ( Im3 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im2 z1) / ( |.z1.| ^2 )))) + (( Im2 (z2 " )) * ( Rea (z1 " )))) + (( Im3 (z2 " )) * ( Im1 (z1 " )))) - (( Im1 (z2 " )) * ( Im3 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im2 z1) / ( |.z1.| ^2 )))) + (( - (( Im2 z2) / ( |.z2.| ^2 ))) * ( Rea (z1 " )))) + (( Im3 (z2 " )) * ( Im1 (z1 " )))) - (( Im1 (z2 " )) * ( Im3 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im2 z1) / ( |.z1.| ^2 )))) + (( - (( Im2 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( Im3 (z2 " )) * ( Im1 (z1 " )))) - (( Im1 (z2 " )) * ( Im3 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im2 z1) / ( |.z1.| ^2 )))) + (( - (( Im2 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( - (( Im3 z2) / ( |.z2.| ^2 ))) * ( Im1 (z1 " )))) - (( Im1 (z2 " )) * ( Im3 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im2 z1) / ( |.z1.| ^2 )))) + (( - (( Im2 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( - (( Im3 z2) / ( |.z2.| ^2 ))) * ( - (( Im1 z1) / ( |.z1.| ^2 ))))) - (( Im1 (z2 " )) * ( Im3 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im2 z1) / ( |.z1.| ^2 )))) + (( - (( Im2 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( - (( Im3 z2) / ( |.z2.| ^2 ))) * ( - (( Im1 z1) / ( |.z1.| ^2 ))))) - (( - (( Im1 z2) / ( |.z2.| ^2 ))) * ( Im3 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im2 z1) / ( |.z1.| ^2 )))) + (( - (( Im2 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( - (( Im3 z2) / ( |.z2.| ^2 ))) * ( - (( Im1 z1) / ( |.z1.| ^2 ))))) - (( - (( Im1 z2) / ( |.z2.| ^2 ))) * ( - (( Im3 z1) / ( |.z1.| ^2 ))))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * (( - ( Im2 z1)) / ( |.z1.| ^2 ))) + ((( - ( Im2 z2)) / ( |.z2.| ^2 )) * (( Rea z1) / ( |.z1.| ^2 )))) + ((( Im3 z2) / ( |.z2.| ^2 )) * (( Im1 z1) / ( |.z1.| ^2 )))) - ((( Im1 z2) / ( |.z2.| ^2 )) * (( Im3 z1) / ( |.z1.| ^2 ))))

 .= (((((( Rea z2) * ( - ( Im2 z1))) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) + ((( - ( Im2 z2)) / ( |.z2.| ^2 )) * (( Rea z1) / ( |.z1.| ^2 )))) + ((( Im3 z2) / ( |.z2.| ^2 )) * (( Im1 z1) / ( |.z1.| ^2 )))) - ((( Im1 z2) / ( |.z2.| ^2 )) * (( Im3 z1) / ( |.z1.| ^2 )))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( - ( Im2 z1))) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) + ((( - ( Im2 z2)) * ( Rea z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) + ((( Im3 z2) / ( |.z2.| ^2 )) * (( Im1 z1) / ( |.z1.| ^2 )))) - ((( Im1 z2) / ( |.z2.| ^2 )) * (( Im3 z1) / ( |.z1.| ^2 )))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( - ( Im2 z1))) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) + ((( - ( Im2 z2)) * ( Rea z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) + ((( Im3 z2) * ( Im1 z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) - ((( Im1 z2) / ( |.z2.| ^2 )) * (( Im3 z1) / ( |.z1.| ^2 )))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( - ( Im2 z1))) + (( - ( Im2 z2)) * ( Rea z1))) + (( Im3 z2) * ( Im1 z1))) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) - ((( Im1 z2) * ( Im3 z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( - ( Im2 z1))) + (( - ( Im2 z2)) * ( Rea z1))) + (( Im3 z2) * ( Im1 z1))) - (( Im1 z2) * ( Im3 z1))) / (( |.z2.| * |.z1.|) ^2 ));



 A3: ((((( Rea (z2 " )) * ( Im3 (z1 " ))) + (( Im3 (z2 " )) * ( Rea (z1 " )))) + (( Im1 (z2 " )) * ( Im2 (z1 " )))) - (( Im2 (z2 " )) * ( Im1 (z1 " )))) = (((((( Rea z2) / ( |.z2.| ^2 )) * ( Im3 (z1 " ))) + (( Im3 (z2 " )) * ( Rea (z1 " )))) + (( Im1 (z2 " )) * ( Im2 (z1 " )))) - (( Im2 (z2 " )) * ( Im1 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im3 z1) / ( |.z1.| ^2 )))) + (( Im3 (z2 " )) * ( Rea (z1 " )))) + (( Im1 (z2 " )) * ( Im2 (z1 " )))) - (( Im2 (z2 " )) * ( Im1 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im3 z1) / ( |.z1.| ^2 )))) + (( - (( Im3 z2) / ( |.z2.| ^2 ))) * ( Rea (z1 " )))) + (( Im1 (z2 " )) * ( Im2 (z1 " )))) - (( Im2 (z2 " )) * ( Im1 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im3 z1) / ( |.z1.| ^2 )))) + (( - (( Im3 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( Im1 (z2 " )) * ( Im2 (z1 " )))) - (( Im2 (z2 " )) * ( Im1 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im3 z1) / ( |.z1.| ^2 )))) + (( - (( Im3 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( - (( Im1 z2) / ( |.z2.| ^2 ))) * ( Im2 (z1 " )))) - (( Im2 (z2 " )) * ( Im1 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im3 z1) / ( |.z1.| ^2 )))) + (( - (( Im3 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( - (( Im1 z2) / ( |.z2.| ^2 ))) * ( - (( Im2 z1) / ( |.z1.| ^2 ))))) - (( Im2 (z2 " )) * ( Im1 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im3 z1) / ( |.z1.| ^2 )))) + (( - (( Im3 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( - (( Im1 z2) / ( |.z2.| ^2 ))) * ( - (( Im2 z1) / ( |.z1.| ^2 ))))) - (( - (( Im2 z2) / ( |.z2.| ^2 ))) * ( Im1 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * ( - (( Im3 z1) / ( |.z1.| ^2 )))) + (( - (( Im3 z2) / ( |.z2.| ^2 ))) * (( Rea z1) / ( |.z1.| ^2 )))) + (( - (( Im1 z2) / ( |.z2.| ^2 ))) * ( - (( Im2 z1) / ( |.z1.| ^2 ))))) - (( - (( Im2 z2) / ( |.z2.| ^2 ))) * ( - (( Im1 z1) / ( |.z1.| ^2 ))))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * (( - ( Im3 z1)) / ( |.z1.| ^2 ))) - ((( Im3 z2) / ( |.z2.| ^2 )) * (( Rea z1) / ( |.z1.| ^2 )))) + ((( Im1 z2) / ( |.z2.| ^2 )) * (( Im2 z1) / ( |.z1.| ^2 )))) - ((( Im2 z2) / ( |.z2.| ^2 )) * (( Im1 z1) / ( |.z1.| ^2 ))))

 .= (((((( Rea z2) * ( - ( Im3 z1))) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) - ((( Im3 z2) / ( |.z2.| ^2 )) * (( Rea z1) / ( |.z1.| ^2 )))) + ((( Im1 z2) / ( |.z2.| ^2 )) * (( Im2 z1) / ( |.z1.| ^2 )))) - ((( Im2 z2) / ( |.z2.| ^2 )) * (( Im1 z1) / ( |.z1.| ^2 )))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( - ( Im3 z1))) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) - ((( Im3 z2) * ( Rea z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) + ((( Im1 z2) / ( |.z2.| ^2 )) * (( Im2 z1) / ( |.z1.| ^2 )))) - ((( Im2 z2) / ( |.z2.| ^2 )) * (( Im1 z1) / ( |.z1.| ^2 )))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( - ( Im3 z1))) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) - ((( Im3 z2) * ( Rea z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) + ((( Im1 z2) * ( Im2 z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) - ((( Im2 z2) / ( |.z2.| ^2 )) * (( Im1 z1) / ( |.z1.| ^2 )))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( - ( Im3 z1))) - (( Im3 z2) * ( Rea z1))) + (( Im1 z2) * ( Im2 z1))) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) - ((( Im2 z2) * ( Im1 z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( - ( Im3 z1))) - (( Im3 z2) * ( Rea z1))) + (( Im1 z2) * ( Im2 z1))) - (( Im2 z2) * ( Im1 z1))) / (( |.z2.| * |.z1.|) ^2 ));

 ((((( Rea (z2 " )) * ( Rea (z1 " ))) - (( Im1 (z2 " )) * ( Im1 (z1 " )))) - (( Im2 (z2 " )) * ( Im2 (z1 " )))) - (( Im3 (z2 " )) * ( Im3 (z1 " )))) = (((((( Rea z2) / ( |.z2.| ^2 )) * ( Rea (z1 " ))) - (( Im1 (z2 " )) * ( Im1 (z1 " )))) - (( Im2 (z2 " )) * ( Im2 (z1 " )))) - (( Im3 (z2 " )) * ( Im3 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * (( Rea z1) / ( |.z1.| ^2 ))) - (( Im1 (z2 " )) * ( Im1 (z1 " )))) - (( Im2 (z2 " )) * ( Im2 (z1 " )))) - (( Im3 (z2 " )) * ( Im3 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * (( Rea z1) / ( |.z1.| ^2 ))) - (( - (( Im1 z2) / ( |.z2.| ^2 ))) * ( Im1 (z1 " )))) - (( Im2 (z2 " )) * ( Im2 (z1 " )))) - (( Im3 (z2 " )) * ( Im3 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * (( Rea z1) / ( |.z1.| ^2 ))) - (( - (( Im1 z2) / ( |.z2.| ^2 ))) * ( - (( Im1 z1) / ( |.z1.| ^2 ))))) - (( Im2 (z2 " )) * ( Im2 (z1 " )))) - (( Im3 (z2 " )) * ( Im3 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * (( Rea z1) / ( |.z1.| ^2 ))) - (( - (( Im1 z2) / ( |.z2.| ^2 ))) * ( - (( Im1 z1) / ( |.z1.| ^2 ))))) - (( - (( Im2 z2) / ( |.z2.| ^2 ))) * ( Im2 (z1 " )))) - (( Im3 (z2 " )) * ( Im3 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * (( Rea z1) / ( |.z1.| ^2 ))) - (( - (( Im1 z2) / ( |.z2.| ^2 ))) * ( - (( Im1 z1) / ( |.z1.| ^2 ))))) - (( - (( Im2 z2) / ( |.z2.| ^2 ))) * ( - (( Im2 z1) / ( |.z1.| ^2 ))))) - (( Im3 (z2 " )) * ( Im3 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * (( Rea z1) / ( |.z1.| ^2 ))) - (( - (( Im1 z2) / ( |.z2.| ^2 ))) * ( - (( Im1 z1) / ( |.z1.| ^2 ))))) - (( - (( Im2 z2) / ( |.z2.| ^2 ))) * ( - (( Im2 z1) / ( |.z1.| ^2 ))))) - (( - (( Im3 z2) / ( |.z2.| ^2 ))) * ( Im3 (z1 " )))) by QUATERN2: 29

 .= (((((( Rea z2) / ( |.z2.| ^2 )) * (( Rea z1) / ( |.z1.| ^2 ))) - (( - (( Im1 z2) / ( |.z2.| ^2 ))) * ( - (( Im1 z1) / ( |.z1.| ^2 ))))) - (( - (( Im2 z2) / ( |.z2.| ^2 ))) * ( - (( Im2 z1) / ( |.z1.| ^2 ))))) - (( - (( Im3 z2) / ( |.z2.| ^2 ))) * ( - (( Im3 z1) / ( |.z1.| ^2 ))))) by QUATERN2: 29

 .= (((((( Rea z2) * ( Rea z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) - ((( Im1 z2) / ( |.z2.| ^2 )) * (( Im1 z1) / ( |.z1.| ^2 )))) - ((( Im2 z2) / ( |.z2.| ^2 )) * (( Im2 z1) / ( |.z1.| ^2 )))) - ((( Im3 z2) / ( |.z2.| ^2 )) * (( Im3 z1) / ( |.z1.| ^2 )))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( Rea z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) - ((( Im1 z2) * ( Im1 z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) - ((( Im2 z2) / ( |.z2.| ^2 )) * (( Im2 z1) / ( |.z1.| ^2 )))) - ((( Im3 z2) / ( |.z2.| ^2 )) * (( Im3 z1) / ( |.z1.| ^2 )))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( Rea z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) - ((( Im1 z2) * ( Im1 z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) - ((( Im2 z2) * ( Im2 z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) - ((( Im3 z2) / ( |.z2.| ^2 )) * (( Im3 z1) / ( |.z1.| ^2 )))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( Rea z1)) - (( Im1 z2) * ( Im1 z1))) - (( Im2 z2) * ( Im2 z1))) / (( |.z2.| ^2 ) * ( |.z1.| ^2 ))) - ((( Im3 z2) * ( Im3 z1)) / (( |.z2.| ^2 ) * ( |.z1.| ^2 )))) by XCMPLX_1: 76

 .= (((((( Rea z2) * ( Rea z1)) - (( Im1 z2) * ( Im1 z1))) - (( Im2 z2) * ( Im2 z1))) - (( Im3 z2) * ( Im3 z1))) / (( |.z2.| * |.z1.|) ^2 ));



 then

 A4: ((z2 " ) * (z1 " )) = ((((((((( Rea z2) * ( Rea z1)) - (( Im1 z2) * ( Im1 z1))) - (( Im2 z2) * ( Im2 z1))) - (( Im3 z2) * ( Im3 z1))) / (( |.z2.| * |.z1.|) ^2 )) + (( - (((((( Rea z2) * ( Im1 z1)) + (( Im1 z2) * ( Rea z1))) - (( Im2 z2) * ( Im3 z1))) + (( Im3 z2) * ( Im2 z1))) / (( |.z2.| * |.z1.|) ^2 ))) * )) + (( - (((((( Rea z2) * ( Im2 z1)) + (( Im2 z2) * ( Rea z1))) - (( Im3 z2) * ( Im1 z1))) + (( Im1 z2) * ( Im3 z1))) / (( |.z2.| * |.z1.|) ^2 ))) * <j> )) + (( - (((((( Rea z2) * ( Im3 z1)) + (( Im3 z2) * ( Rea z1))) - (( Im1 z2) * ( Im2 z1))) + (( Im2 z2) * ( Im1 z1))) / (( |.z2.| * |.z1.|) ^2 ))) * <k> )) by A1, A2, A3, QUATERNI: 93

 .= ((((((((( Rea z2) * ( Rea z1)) - (( Im1 z2) * ( Im1 z1))) - (( Im2 z2) * ( Im2 z1))) - (( Im3 z2) * ( Im3 z1))) / (( |.z2.| * |.z1.|) ^2 )) + ( - ((((((( Rea z2) * ( Im1 z1)) + (( Im1 z2) * ( Rea z1))) - (( Im2 z2) * ( Im3 z1))) + (( Im3 z2) * ( Im2 z1))) / (( |.z2.| * |.z1.|) ^2 )) * ))) + (( - (((((( Rea z2) * ( Im2 z1)) + (( Im2 z2) * ( Rea z1))) - (( Im3 z2) * ( Im1 z1))) + (( Im1 z2) * ( Im3 z1))) / (( |.z2.| * |.z1.|) ^2 ))) * <j> )) + (( - (((((( Rea z2) * ( Im3 z1)) + (( Im3 z2) * ( Rea z1))) - (( Im1 z2) * ( Im2 z1))) + (( Im2 z2) * ( Im1 z1))) / (( |.z2.| * |.z1.|) ^2 ))) * <k> )) by QUATERN2: 9

 .= ((((((((( Rea z2) * ( Rea z1)) - (( Im1 z2) * ( Im1 z1))) - (( Im2 z2) * ( Im2 z1))) - (( Im3 z2) * ( Im3 z1))) / (( |.z2.| * |.z1.|) ^2 )) + ( - ((((((( Rea z2) * ( Im1 z1)) + (( Im1 z2) * ( Rea z1))) - (( Im2 z2) * ( Im3 z1))) + (( Im3 z2) * ( Im2 z1))) / (( |.z2.| * |.z1.|) ^2 )) * ))) + ( - ((((((( Rea z2) * ( Im2 z1)) + (( Im2 z2) * ( Rea z1))) - (( Im3 z2) * ( Im1 z1))) + (( Im1 z2) * ( Im3 z1))) / (( |.z2.| * |.z1.|) ^2 )) * <j> ))) + (( - (((((( Rea z2) * ( Im3 z1)) + (( Im3 z2) * ( Rea z1))) - (( Im1 z2) * ( Im2 z1))) + (( Im2 z2) * ( Im1 z1))) / (( |.z2.| * |.z1.|) ^2 ))) * <k> )) by QUATERN2: 9

 .= ((((((((( Rea z2) * ( Rea z1)) - (( Im1 z2) * ( Im1 z1))) - (( Im2 z2) * ( Im2 z1))) - (( Im3 z2) * ( Im3 z1))) / (( |.z2.| * |.z1.|) ^2 )) - ((((((( Rea z2) * ( Im1 z1)) + (( Im1 z2) * ( Rea z1))) - (( Im2 z2) * ( Im3 z1))) + (( Im3 z2) * ( Im2 z1))) / (( |.z2.| * |.z1.|) ^2 )) * )) - ((((((( Rea z2) * ( Im2 z1)) + (( Im2 z2) * ( Rea z1))) - (( Im3 z2) * ( Im1 z1))) + (( Im1 z2) * ( Im3 z1))) / (( |.z2.| * |.z1.|) ^2 )) * <j> )) - ((((((( Rea z2) * ( Im3 z1)) + (( Im3 z2) * ( Rea z1))) - (( Im1 z2) * ( Im2 z1))) + (( Im2 z2) * ( Im1 z1))) / (( |.z2.| * |.z1.|) ^2 )) * <k> )) by QUATERN2: 9;

 (z3 " ) = ((((( Rea z3) / ( |.z3.| ^2 )) - ((( Im1 z3) / ( |.z3.| ^2 )) * )) - ((( Im2 z3) / ( |.z3.| ^2 )) * <j> )) - ((( Im3 z3) / ( |.z3.| ^2 )) * <k> )) by QUATERN2: 28

 .= ((((( Rea z3) / (( |.z1.| * |.z2.|) ^2 )) - ((( Im1 z3) / ( |.z3.| ^2 )) * )) - ((( Im2 z3) / ( |.z3.| ^2 )) * <j> )) - ((( Im3 z3) / ( |.z3.| ^2 )) * <k> )) by QUATERNI: 87

 .= ((((( Rea z3) / (( |.z1.| * |.z2.|) ^2 )) - ((( Im1 z3) / (( |.z1.| * |.z2.|) ^2 )) * )) - ((( Im2 z3) / ( |.z3.| ^2 )) * <j> )) - ((( Im3 z3) / ( |.z3.| ^2 )) * <k> )) by QUATERNI: 87

 .= ((((( Rea z3) / (( |.z1.| * |.z2.|) ^2 )) - ((( Im1 z3) / (( |.z1.| * |.z2.|) ^2 )) * )) - ((( Im2 z3) / (( |.z1.| * |.z2.|) ^2 )) * <j> )) - ((( Im3 z3) / ( |.z3.| ^2 )) * <k> )) by QUATERNI: 87

 .= ((((( Rea z3) / (( |.z1.| * |.z2.|) ^2 )) - ((( Im1 z3) / (( |.z1.| * |.z2.|) ^2 )) * )) - ((( Im2 z3) / (( |.z1.| * |.z2.|) ^2 )) * <j> )) - ((( Im3 z3) / (( |.z1.| * |.z2.|) ^2 )) * <k> )) by QUATERNI: 87

 .= ((((((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))) / (( |.z1.| * |.z2.|) ^2 )) - ((( Im1 (z1 * z2)) / (( |.z1.| * |.z2.|) ^2 )) * )) - ((( Im2 (z1 * z2)) / (( |.z1.| * |.z2.|) ^2 )) * <j> )) - ((( Im3 (z1 * z2)) / (( |.z1.| * |.z2.|) ^2 )) * <k> )) by QUATERNI: 97

 .= ((((((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))) / (( |.z1.| * |.z2.|) ^2 )) - ((((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))) / (( |.z1.| * |.z2.|) ^2 )) * )) - ((( Im2 (z1 * z2)) / (( |.z1.| * |.z2.|) ^2 )) * <j> )) - ((( Im3 (z1 * z2)) / (( |.z1.| * |.z2.|) ^2 )) * <k> )) by QUATERNI: 97

 .= ((((((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))) / (( |.z1.| * |.z2.|) ^2 )) - ((((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))) / (( |.z1.| * |.z2.|) ^2 )) * )) - ((((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2))) / (( |.z1.| * |.z2.|) ^2 )) * <j> )) - ((( Im3 (z1 * z2)) / (( |.z1.| * |.z2.|) ^2 )) * <k> )) by QUATERNI: 97

 .= ((((((((( Rea z1) * ( Rea z2)) - (( Im1 z1) * ( Im1 z2))) - (( Im2 z1) * ( Im2 z2))) - (( Im3 z1) * ( Im3 z2))) / (( |.z1.| * |.z2.|) ^2 )) - ((((((( Rea z1) * ( Im1 z2)) + (( Im1 z1) * ( Rea z2))) + (( Im2 z1) * ( Im3 z2))) - (( Im3 z1) * ( Im2 z2))) / (( |.z1.| * |.z2.|) ^2 )) * )) - ((((((( Rea z1) * ( Im2 z2)) + (( Im2 z1) * ( Rea z2))) + (( Im3 z1) * ( Im1 z2))) - (( Im1 z1) * ( Im3 z2))) / (( |.z1.| * |.z2.|) ^2 )) * <j> )) - ((((((( Rea z1) * ( Im3 z2)) + (( Im3 z1) * ( Rea z2))) + (( Im1 z1) * ( Im2 z2))) - (( Im2 z1) * ( Im1 z2))) / (( |.z1.| * |.z2.|) ^2 )) * <k> )) by QUATERNI: 97;

 hence thesis by A4;

 end;

 theorem :: QUATERN3:47

 ((z *' ) " ) = ((z " ) *' )

 proof

 ( Im1 ((z *' ) " )) = ( - (( Im1 (z *' )) / ( |.(z *' ).| ^2 ))) by QUATERN2: 29;

 then

 A1: ( Im1 ((z *' ) " )) = ( - (( - ( Im1 z)) / ( |.(z *' ).| ^2 ))) by QUATERNI: 44;

 ( Im2 ((z *' ) " )) = ( - (( Im2 (z *' )) / ( |.(z *' ).| ^2 ))) by QUATERN2: 29;

 then

 A2: ( Im2 ((z *' ) " )) = ( - (( - ( Im2 z)) / ( |.(z *' ).| ^2 ))) by QUATERNI: 44;

 ( Im2 ((z " ) *' )) = ( - ( Im2 (z " ))) by QUATERNI: 44;

 then ( Im2 ((z " ) *' )) = ( - ( - (( Im2 z) / ( |.z.| ^2 )))) by QUATERN2: 29;

 then

 A3: ( Im2 ((z " ) *' )) = ( - ( - (( Im2 z) / ( |.(z *' ).| ^2 )))) by QUATERNI: 73;

 ( Im1 ((z " ) *' )) = ( - ( Im1 (z " ))) by QUATERNI: 44;

 then ( Im1 ((z " ) *' )) = ( - ( - (( Im1 z) / ( |.z.| ^2 )))) by QUATERN2: 29;

 then

 A4: ( Im1 ((z " ) *' )) = ( - ( - (( Im1 z) / ( |.(z *' ).| ^2 )))) by QUATERNI: 73;

 ( Im3 ((z " ) *' )) = ( - ( Im3 (z " ))) by QUATERNI: 44;

 then ( Im3 ((z " ) *' )) = ( - ( - (( Im3 z) / ( |.z.| ^2 )))) by QUATERN2: 29;

 then

 A5: ( Im3 ((z " ) *' )) = ( - ( - (( Im3 z) / ( |.(z *' ).| ^2 )))) by QUATERNI: 73;

 ( Rea ((z " ) *' )) = ( Rea (z " )) by QUATERNI: 44;

 then ( Rea ((z " ) *' )) = (( Rea z) / ( |.z.| ^2 )) by QUATERN2: 29;

 then

 A6: ( Rea ((z " ) *' )) = (( Rea z) / ( |.(z *' ).| ^2 )) by QUATERNI: 73;

 ( Im3 ((z *' ) " )) = ( - (( Im3 (z *' )) / ( |.(z *' ).| ^2 ))) by QUATERN2: 29;

 then

 A7: ( Im3 ((z *' ) " )) = ( - (( - ( Im3 z)) / ( |.(z *' ).| ^2 ))) by QUATERNI: 44;

 ( Rea ((z *' ) " )) = (( Rea (z *' )) / ( |.(z *' ).| ^2 )) by QUATERN2: 29;

 then ( Rea ((z *' ) " )) = (( Rea z) / ( |.(z *' ).| ^2 )) by QUATERNI: 44;

 hence thesis by A1, A2, A7, A6, A4, A3, A5, QUATERNI: 25;

 end;

 theorem :: QUATERN3:48

 ( 1q " ) = 1q

 proof



 A1: ( Im3 ( 1q " )) = ( - (( Im3 1q ) / ( |. 1q .| ^2 ))) by QUATERN2: 29

 .= 0 by QUATERNI: 29;



 A2: ( Im2 ( 1q " )) = ( - (( Im2 1q ) / ( |. 1q .| ^2 ))) by QUATERN2: 29

 .= 0 by QUATERNI: 29;



 A3: ( Im1 ( 1q " )) = ( - (( Im1 1q ) / ( |. 1q .| ^2 ))) by QUATERN2: 29

 .= 0 by QUATERNI: 29;

 ( Rea ( 1q " )) = (( Rea 1q ) / ( |. 1q .| ^2 )) by QUATERN2: 29

 .= 1 by QUATERNI: 29, QUATERNI: 68;

 then ( 1q " ) = [*1, 0 , 0 , 0 *] by A3, A2, A1, QUATERNI: 24;

 hence thesis by QUATERNI: 24, QUATERNI: 29;

 end;

 theorem :: QUATERN3:49

 |.z1.| = |.z2.| & |.z1.| <> 0 & (z1 " ) = (z2 " ) implies z1 = z2

 proof

 assume that

 A1: |.z1.| = |.z2.| and

 A2: |.z1.| <> 0 and

 A3: (z1 " ) = (z2 " );



 A4: ( |.z1.| ^2 ) <> 0 by A2, XCMPLX_1: 6;

 ( Im3 (z1 " )) = ( - (( Im3 z1) / ( |.z1.| ^2 ))) by QUATERN2: 29;

 then ( - (( Im3 z1) / ( |.z1.| ^2 ))) = ( - (( Im3 z2) / ( |.z2.| ^2 ))) by A3, QUATERN2: 29;

 then

 A5: ( Im3 z1) = ( Im3 z2) by A1, A4, XCMPLX_1: 53;

 ( Im2 (z1 " )) = ( - (( Im2 z1) / ( |.z1.| ^2 ))) by QUATERN2: 29;

 then ( - (( Im2 z1) / ( |.z1.| ^2 ))) = ( - (( Im2 z2) / ( |.z2.| ^2 ))) by A3, QUATERN2: 29;

 then

 A6: ( Im2 z1) = ( Im2 z2) by A1, A4, XCMPLX_1: 53;

 ( Im1 (z1 " )) = ( - (( Im1 z1) / ( |.z1.| ^2 ))) by QUATERN2: 29;

 then ( - (( Im1 z1) / ( |.z1.| ^2 ))) = ( - (( Im1 z2) / ( |.z2.| ^2 ))) by A3, QUATERN2: 29;

 then

 A7: ( Im1 z1) = ( Im1 z2) by A1, A4, XCMPLX_1: 53;

 ( Rea (z1 " )) = (( Rea z1) / ( |.z1.| ^2 )) by QUATERN2: 29;

 then (( Rea z1) / ( |.z1.| ^2 )) = (( Rea z2) / ( |.z2.| ^2 )) by A3, QUATERN2: 29;

 then ( Rea z1) = ( Rea z2) by A1, A4, XCMPLX_1: 53;

 hence thesis by A7, A6, A5, QUATERNI: 25;

 end;

 theorem :: QUATERN3:50

 ((z1 - z2) * (z3 + z4)) = ((((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4))

 proof

 ((z1 - z2) * (z3 + z4)) = (((z1 - z2) * z3) + ((z1 - z2) * z4)) by QUATERN2: 17

 .= (((z1 * z3) - (z2 * z3)) + ((z1 - z2) * z4)) by QUATERN2: 23

 .= (((z1 * z3) - (z2 * z3)) + ((z1 * z4) - (z2 * z4))) by QUATERN2: 23

 .= ((((z1 * z3) - (z2 * z3)) + (z1 * z4)) - (z2 * z4)) by QUATERN2: 2;

 hence thesis;

 end;

 theorem :: QUATERN3:51

 ((z1 + z2) * (z3 + z4)) = ((((z1 * z3) + (z2 * z3)) + (z1 * z4)) + (z2 * z4))

 proof

 ((z1 + z2) * (z3 + z4)) = (((z1 + z2) * z3) + ((z1 + z2) * z4)) by QUATERN2: 17

 .= (((z1 * z3) + (z2 * z3)) + ((z1 + z2) * z4)) by QUATERN2: 18

 .= (((z1 * z3) + (z2 * z3)) + ((z1 * z4) + (z2 * z4))) by QUATERN2: 18

 .= ((((z1 * z3) + (z2 * z3)) + (z1 * z4)) + (z2 * z4)) by QUATERN2: 2;

 hence thesis;

 end;

 theorem :: QUATERN3:52



 Th52: ( - (z1 + z2)) = (( - z1) - z2)

 proof



 A1: (( - z1) - z2) = ((( - 1q ) * z1) - z2) by QUATERN2: 19

 .= ((( - 1q ) * z1) + (( - 1q ) * z2)) by QUATERN2: 19;

 ( - (z1 + z2)) = (( - 1q ) * (z1 + z2)) by QUATERN2: 19

 .= ((( - 1q ) * z1) + (( - 1q ) * z2)) by QUATERN2: 17;

 hence thesis by A1;

 end;

 theorem :: QUATERN3:53



 Th53: ( - (z1 - z2)) = (( - z1) + z2)

 proof

 ( - (z1 - z2)) = (( - 1q ) * (z1 - z2)) by QUATERN2: 19

 .= ((( - 1q ) * z1) - (( - 1q ) * z2)) by QUATERN2: 24

 .= ((( - 1q ) * z1) - ( - z2)) by QUATERN2: 19;

 hence thesis by QUATERN2: 19;

 end;

 theorem :: QUATERN3:54



 Th54: (z - (z1 + z2)) = ((z - z1) - z2)

 proof



 A1: ((z - z1) - z2) = ((z + (( - 1q ) * z1)) + ( - z2)) by QUATERN2: 19

 .= ((z + (( - 1q ) * z1)) + (( - 1q ) * z2)) by QUATERN2: 19;

 ( - (z1 + z2)) = (( - 1q ) * (z1 + z2)) by QUATERN2: 19

 .= ((( - 1q ) * z1) + (( - 1q ) * z2)) by QUATERN2: 17;

 hence thesis by A1, QUATERN2: 2;

 end;

 theorem :: QUATERN3:55



 Th55: (z - (z1 - z2)) = ((z - z1) + z2)

 proof

 ( - (z1 - z2)) = (( - 1q ) * (z1 - z2)) by QUATERN2: 19

 .= ((( - 1q ) * z1) - (( - 1q ) * z2)) by QUATERN2: 24;



 then (z - (z1 - z2)) = (z + ((( - 1q ) * z1) - ( - z2))) by QUATERN2: 19

 .= ((z + (( - 1q ) * z1)) + z2) by QUATERN2: 2;

 hence thesis by QUATERN2: 19;

 end;

 theorem :: QUATERN3:56

 ((z1 + z2) * (z3 - z4)) = ((((z1 * z3) + (z2 * z3)) - (z1 * z4)) - (z2 * z4))

 proof

 ((z1 + z2) * (z3 - z4)) = (((z1 + z2) * z3) - ((z1 + z2) * z4)) by QUATERN2: 24

 .= (((z1 * z3) + (z2 * z3)) - ((z1 + z2) * z4)) by QUATERN2: 18

 .= (((z1 * z3) + (z2 * z3)) - ((z1 * z4) + (z2 * z4))) by QUATERN2: 18

 .= ((((z1 * z3) + (z2 * z3)) - (z1 * z4)) - (z2 * z4)) by Th54;

 hence thesis;

 end;

 theorem :: QUATERN3:57



 Th57: ((z1 - z2) * (z3 - z4)) = ((((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4))

 proof

 ((z1 - z2) * (z3 - z4)) = (((z1 - z2) * z3) - ((z1 - z2) * z4)) by QUATERN2: 24

 .= (((z1 * z3) - (z2 * z3)) - ((z1 - z2) * z4)) by QUATERN2: 23

 .= (((z1 * z3) - (z2 * z3)) - ((z1 * z4) - (z2 * z4))) by QUATERN2: 23

 .= ((((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4)) by Th55;

 hence thesis;

 end;

 theorem :: QUATERN3:58

 ( - ((z1 + z2) + z3)) = ((( - z1) - z2) - z3)

 proof

 ( - ((z1 + z2) + z3)) = ( - (z1 + (z2 + z3))) by QUATERN2: 2

 .= (( - z1) - (z2 + z3)) by Th52

 .= ((( - z1) - z2) - z3) by Th54;

 hence thesis;

 end;

 theorem :: QUATERN3:59

 ( - ((z1 - z2) - z3)) = ((( - z1) + z2) + z3)

 proof

 ( - ((z1 - z2) - z3)) = (( - (z1 - z2)) + z3) by Th53

 .= ((( - z1) + z2) + z3) by Th53;

 hence thesis;

 end;

 theorem :: QUATERN3:60

 ( - ((z1 - z2) + z3)) = ((( - z1) + z2) - z3)

 proof

 ( - ((z1 - z2) + z3)) = (( - (z1 - z2)) - z3) by Th52

 .= ((( - z1) + z2) - z3) by Th53;

 hence thesis;

 end;

 theorem :: QUATERN3:61

 ( - ((z1 + z2) - z3)) = ((( - z1) - z2) + z3)

 proof

 ( - ((z1 + z2) - z3)) = (( - (z1 + z2)) + z3) by Th53

 .= ((( - z1) - z2) + z3) by Th52;

 hence thesis;

 end;

 theorem :: QUATERN3:62

 (z1 + z) = (z2 + z) implies z1 = z2

 proof



 A1: ( Rea (z1 + z)) = (( Rea z1) + ( Rea z)) & ( Im1 (z1 + z)) = (( Im1 z1) + ( Im1 z)) by QUATERNI: 36;



 A2: ( Im2 (z1 + z)) = (( Im2 z1) + ( Im2 z)) & ( Im3 (z1 + z)) = (( Im3 z1) + ( Im3 z)) by QUATERNI: 36;



 A3: ( Im2 (z2 + z)) = (( Im2 z2) + ( Im2 z)) & ( Im3 (z2 + z)) = (( Im3 z2) + ( Im3 z)) by QUATERNI: 36;



 A4: ( Rea (z2 + z)) = (( Rea z2) + ( Rea z)) & ( Im1 (z2 + z)) = (( Im1 z2) + ( Im1 z)) by QUATERNI: 36;

 assume (z1 + z) = (z2 + z);

 hence thesis by A1, A2, A4, A3, QUATERNI: 25;

 end;

 theorem :: QUATERN3:63

 (z1 - z) = (z2 - z) implies z1 = z2

 proof



 A1: ( Rea (z1 - z)) = (( Rea z1) - ( Rea z)) & ( Im1 (z1 - z)) = (( Im1 z1) - ( Im1 z)) by QUATERNI: 42;



 A2: ( Im2 (z1 - z)) = (( Im2 z1) - ( Im2 z)) & ( Im3 (z1 - z)) = (( Im3 z1) - ( Im3 z)) by QUATERNI: 42;



 A3: ( Im2 (z2 - z)) = (( Im2 z2) - ( Im2 z)) & ( Im3 (z2 - z)) = (( Im3 z2) - ( Im3 z)) by QUATERNI: 42;



 A4: ( Rea (z2 - z)) = (( Rea z2) - ( Rea z)) & ( Im1 (z2 - z)) = (( Im1 z2) - ( Im1 z)) by QUATERNI: 42;

 assume (z1 - z) = (z2 - z);

 hence thesis by A1, A2, A4, A3, QUATERNI: 25;

 end;

 theorem :: QUATERN3:64

 (((z1 + z2) - z3) * z4) = (((z1 * z4) + (z2 * z4)) - (z3 * z4))

 proof

 (((z1 + z2) - z3) * z4) = (((z1 + z2) * z4) - (z3 * z4)) by QUATERN2: 23

 .= (((z1 * z4) + (z2 * z4)) - (z3 * z4)) by QUATERN2: 18;

 hence thesis;

 end;

 theorem :: QUATERN3:65

 (((z1 - z2) + z3) * z4) = (((z1 * z4) - (z2 * z4)) + (z3 * z4))

 proof

 (((z1 - z2) + z3) * z4) = (((z1 - z2) * z4) + (z3 * z4)) by QUATERN2: 18

 .= (((z1 * z4) - (z2 * z4)) + (z3 * z4)) by QUATERN2: 23;

 hence thesis;

 end;

 theorem :: QUATERN3:66

 (((z1 - z2) - z3) * z4) = (((z1 * z4) - (z2 * z4)) - (z3 * z4))

 proof

 (((z1 - z2) - z3) * z4) = (((z1 - z2) * z4) - (z3 * z4)) by QUATERN2: 23

 .= (((z1 * z4) - (z2 * z4)) - (z3 * z4)) by QUATERN2: 23;

 hence thesis;

 end;

 theorem :: QUATERN3:67

 (((z1 + z2) + z3) * z4) = (((z1 * z4) + (z2 * z4)) + (z3 * z4))

 proof

 (((z1 + z2) + z3) * z4) = (((z1 + z2) * z4) + (z3 * z4)) by QUATERN2: 18

 .= (((z1 * z4) + (z2 * z4)) + (z3 * z4)) by QUATERN2: 18;

 hence thesis;

 end;

 theorem :: QUATERN3:68

 ((z1 - z2) * z3) = ((z2 - z1) * ( - z3))

 proof

 ((z2 - z1) * ( - z3)) = ((z2 * ( - z3)) - (z1 * ( - z3))) by QUATERN2: 23

 .= (( - (z2 * z3)) - (z1 * ( - z3))) by QUATERN2: 21

 .= (( - (z2 * z3)) - ( - (z1 * z3))) by QUATERN2: 21

 .= ((z1 * z3) - (z2 * z3));

 hence thesis by QUATERN2: 23;

 end;

 theorem :: QUATERN3:69

 (z3 * (z1 - z2)) = (( - z3) * (z2 - z1))

 proof

 (( - z3) * (z2 - z1)) = ((( - z3) * z2) - (( - z3) * z1)) by QUATERN2: 24

 .= (( - (z3 * z2)) - (( - z3) * z1)) by QUATERN2: 20

 .= (( - (z3 * z2)) - ( - (z3 * z1))) by QUATERN2: 20

 .= ((z3 * z1) - (z3 * z2));

 hence thesis by QUATERN2: 24;

 end;

 theorem :: QUATERN3:70



 Th70: (((z1 - z2) - z3) + z4) = (((z4 - z3) - z2) + z1)

 proof

 ( Im1 (((z1 - z2) - z3) + z4)) = (( Im1 ((z1 - z2) - z3)) + ( Im1 z4)) by QUATERNI: 36;

 then ( Im1 (((z1 - z2) - z3) + z4)) = ((( Im1 (z1 - z2)) - ( Im1 z3)) + ( Im1 z4)) by QUATERNI: 42;

 then

 A1: ( Im1 (((z1 - z2) - z3) + z4)) = (((( Im1 z1) - ( Im1 z2)) - ( Im1 z3)) + ( Im1 z4)) by QUATERNI: 42;

 ( Im2 (((z1 - z2) - z3) + z4)) = (( Im2 ((z1 - z2) - z3)) + ( Im2 z4)) by QUATERNI: 36;

 then ( Im2 (((z1 - z2) - z3) + z4)) = ((( Im2 (z1 - z2)) - ( Im2 z3)) + ( Im2 z4)) by QUATERNI: 42;

 then

 A2: ( Im2 (((z1 - z2) - z3) + z4)) = (((( Im2 z1) - ( Im2 z2)) - ( Im2 z3)) + ( Im2 z4)) by QUATERNI: 42;

 ( Im2 (((z4 - z3) - z2) + z1)) = (( Im2 ((z4 - z3) - z2)) + ( Im2 z1)) by QUATERNI: 36;

 then ( Im2 (((z4 - z3) - z2) + z1)) = ((( Im2 (z4 - z3)) - ( Im2 z2)) + ( Im2 z1)) by QUATERNI: 42;

 then

 A3: ( Im2 (((z4 - z3) - z2) + z1)) = (((( Im2 z4) - ( Im2 z3)) - ( Im2 z2)) + ( Im2 z1)) by QUATERNI: 42;

 ( Im1 (((z4 - z3) - z2) + z1)) = (( Im1 ((z4 - z3) - z2)) + ( Im1 z1)) by QUATERNI: 36;

 then ( Im1 (((z4 - z3) - z2) + z1)) = ((( Im1 (z4 - z3)) - ( Im1 z2)) + ( Im1 z1)) by QUATERNI: 42;

 then

 A4: ( Im1 (((z4 - z3) - z2) + z1)) = (((( Im1 z4) - ( Im1 z3)) - ( Im1 z2)) + ( Im1 z1)) by QUATERNI: 42;

 ( Im3 (((z4 - z3) - z2) + z1)) = (( Im3 ((z4 - z3) - z2)) + ( Im3 z1)) by QUATERNI: 36;

 then ( Im3 (((z4 - z3) - z2) + z1)) = ((( Im3 (z4 - z3)) - ( Im3 z2)) + ( Im3 z1)) by QUATERNI: 42;

 then

 A5: ( Im3 (((z4 - z3) - z2) + z1)) = (((( Im3 z4) - ( Im3 z3)) - ( Im3 z2)) + ( Im3 z1)) by QUATERNI: 42;

 ( Rea (((z4 - z3) - z2) + z1)) = (( Rea ((z4 - z3) - z2)) + ( Rea z1)) by QUATERNI: 36;

 then ( Rea (((z4 - z3) - z2) + z1)) = ((( Rea (z4 - z3)) - ( Rea z2)) + ( Rea z1)) by QUATERNI: 42;

 then

 A6: ( Rea (((z4 - z3) - z2) + z1)) = (((( Rea z4) - ( Rea z3)) - ( Rea z2)) + ( Rea z1)) by QUATERNI: 42;

 ( Im3 (((z1 - z2) - z3) + z4)) = (( Im3 ((z1 - z2) - z3)) + ( Im3 z4)) by QUATERNI: 36;

 then ( Im3 (((z1 - z2) - z3) + z4)) = ((( Im3 (z1 - z2)) - ( Im3 z3)) + ( Im3 z4)) by QUATERNI: 42;

 then

 A7: ( Im3 (((z1 - z2) - z3) + z4)) = (((( Im3 z1) - ( Im3 z2)) - ( Im3 z3)) + ( Im3 z4)) by QUATERNI: 42;

 ( Rea (((z1 - z2) - z3) + z4)) = (( Rea ((z1 - z2) - z3)) + ( Rea z4)) by QUATERNI: 36;

 then ( Rea (((z1 - z2) - z3) + z4)) = ((( Rea (z1 - z2)) - ( Rea z3)) + ( Rea z4)) by QUATERNI: 42;

 then ( Rea (((z1 - z2) - z3) + z4)) = (((( Rea z1) - ( Rea z2)) - ( Rea z3)) + ( Rea z4)) by QUATERNI: 42;

 hence thesis by A1, A2, A7, A6, A4, A3, A5, QUATERNI: 25;

 end;

 theorem :: QUATERN3:71

 ((z1 - z2) * (z3 - z4)) = ((z2 - z1) * (z4 - z3))

 proof

 ((z2 - z1) * (z4 - z3)) = (((z2 - z1) * z4) - ((z2 - z1) * z3)) by QUATERN2: 24

 .= (((z2 * z4) - (z1 * z4)) - ((z2 - z1) * z3)) by QUATERN2: 23

 .= (((z2 * z4) - (z1 * z4)) - ((z2 * z3) - (z1 * z3))) by QUATERN2: 23

 .= ((((z2 * z4) - (z1 * z4)) - (z2 * z3)) + (z1 * z3)) by Th55

 .= ((((z1 * z3) - (z2 * z3)) - (z1 * z4)) + (z2 * z4)) by Th70;

 hence thesis by Th57;

 end;

 theorem :: QUATERN3:72

 ((z - z1) - z2) = ((z - z2) - z1)

 proof

 ( Im1 ((z - z1) - z2)) = (( Im1 (z - z1)) - ( Im1 z2)) by QUATERNI: 42;

 then

 A1: ( Im1 ((z - z1) - z2)) = ((( Im1 z) - ( Im1 z1)) - ( Im1 z2)) by QUATERNI: 42;

 ( Im2 ((z - z1) - z2)) = (( Im2 (z - z1)) - ( Im2 z2)) by QUATERNI: 42;

 then

 A2: ( Im2 ((z - z1) - z2)) = ((( Im2 z) - ( Im2 z1)) - ( Im2 z2)) by QUATERNI: 42;

 ( Im2 ((z - z2) - z1)) = (( Im2 (z - z2)) - ( Im2 z1)) by QUATERNI: 42;

 then

 A3: ( Im2 ((z - z2) - z1)) = ((( Im2 z) - ( Im2 z2)) - ( Im2 z1)) by QUATERNI: 42;

 ( Im1 ((z - z2) - z1)) = (( Im1 (z - z2)) - ( Im1 z1)) by QUATERNI: 42;

 then

 A4: ( Im1 ((z - z2) - z1)) = ((( Im1 z) - ( Im1 z2)) - ( Im1 z1)) by QUATERNI: 42;

 ( Im3 ((z - z2) - z1)) = (( Im3 (z - z2)) - ( Im3 z1)) by QUATERNI: 42;

 then

 A5: ( Im3 ((z - z2) - z1)) = ((( Im3 z) - ( Im3 z2)) - ( Im3 z1)) by QUATERNI: 42;

 ( Rea ((z - z2) - z1)) = (( Rea (z - z2)) - ( Rea z1)) by QUATERNI: 42;

 then

 A6: ( Rea ((z - z2) - z1)) = ((( Rea z) - ( Rea z2)) - ( Rea z1)) by QUATERNI: 42;

 ( Im3 ((z - z1) - z2)) = (( Im3 (z - z1)) - ( Im3 z2)) by QUATERNI: 42;

 then

 A7: ( Im3 ((z - z1) - z2)) = ((( Im3 z) - ( Im3 z1)) - ( Im3 z2)) by QUATERNI: 42;

 ( Rea ((z - z1) - z2)) = (( Rea (z - z1)) - ( Rea z2)) by QUATERNI: 42;

 then ( Rea ((z - z1) - z2)) = ((( Rea z) - ( Rea z1)) - ( Rea z2)) by QUATERNI: 42;

 hence thesis by A1, A2, A7, A6, A4, A3, A5, QUATERNI: 25;

 end;

 theorem :: QUATERN3:73

 (z " ) = [*(( Rea z) / ( |.z.| ^2 )), ( - (( Im1 z) / ( |.z.| ^2 ))), ( - (( Im2 z) / ( |.z.| ^2 ))), ( - (( Im3 z) / ( |.z.| ^2 )))*]

 proof

 (z " ) = [*( Rea (z " )), ( Im1 (z " )), ( Im2 (z " )), ( Im3 (z " ))*] by QUATERNI: 24

 .= [*(( Rea z) / ( |.z.| ^2 )), ( Im1 (z " )), ( Im2 (z " )), ( Im3 (z " ))*] by QUATERN2: 29

 .= [*(( Rea z) / ( |.z.| ^2 )), ( - (( Im1 z) / ( |.z.| ^2 ))), ( Im2 (z " )), ( Im3 (z " ))*] by QUATERN2: 29

 .= [*(( Rea z) / ( |.z.| ^2 )), ( - (( Im1 z) / ( |.z.| ^2 ))), ( - (( Im2 z) / ( |.z.| ^2 ))), ( Im3 (z " ))*] by QUATERN2: 29

 .= [*(( Rea z) / ( |.z.| ^2 )), ( - (( Im1 z) / ( |.z.| ^2 ))), ( - (( Im2 z) / ( |.z.| ^2 ))), ( - (( Im3 z) / ( |.z.| ^2 )))*] by QUATERN2: 29;

 hence thesis;

 end;

 theorem :: QUATERN3:74

 (z1 / z2) = [*(((((( Rea z2) * ( Rea z1)) + (( Im1 z1) * ( Im1 z2))) + (( Im2 z2) * ( Im2 z1))) + (( Im3 z2) * ( Im3 z1))) / ( |.z2.| ^2 )), (((((( Rea z2) * ( Im1 z1)) - (( Im1 z2) * ( Rea z1))) - (( Im2 z2) * ( Im3 z1))) + (( Im3 z2) * ( Im2 z1))) / ( |.z2.| ^2 )), (((((( Rea z2) * ( Im2 z1)) + (( Im1 z2) * ( Im3 z1))) - (( Im2 z2) * ( Rea z1))) - (( Im3 z2) * ( Im1 z1))) / ( |.z2.| ^2 )), (((((( Rea z2) * ( Im3 z1)) - (( Im1 z2) * ( Im2 z1))) + (( Im2 z2) * ( Im1 z1))) - (( Im3 z2) * ( Rea z1))) / ( |.z2.| ^2 ))*]

 proof

 (z1 / z2) = [*( Rea (z1 / z2)), ( Im1 (z1 / z2)), ( Im2 (z1 / z2)), ( Im3 (z1 / z2))*] by QUATERNI: 24

 .= [*(((((( Rea z2) * ( Rea z1)) + (( Im1 z1) * ( Im1 z2))) + (( Im2 z2) * ( Im2 z1))) + (( Im3 z2) * ( Im3 z1))) / ( |.z2.| ^2 )), ( Im1 (z1 / z2)), ( Im2 (z1 / z2)), ( Im3 (z1 / z2))*] by QUATERN2: 30

 .= [*(((((( Rea z2) * ( Rea z1)) + (( Im1 z1) * ( Im1 z2))) + (( Im2 z2) * ( Im2 z1))) + (( Im3 z2) * ( Im3 z1))) / ( |.z2.| ^2 )), (((((( Rea z2) * ( Im1 z1)) - (( Im1 z2) * ( Rea z1))) - (( Im2 z2) * ( Im3 z1))) + (( Im3 z2) * ( Im2 z1))) / ( |.z2.| ^2 )), ( Im2 (z1 / z2)), ( Im3 (z1 / z2))*] by QUATERN2: 30

 .= [*(((((( Rea z2) * ( Rea z1)) + (( Im1 z1) * ( Im1 z2))) + (( Im2 z2) * ( Im2 z1))) + (( Im3 z2) * ( Im3 z1))) / ( |.z2.| ^2 )), (((((( Rea z2) * ( Im1 z1)) - (( Im1 z2) * ( Rea z1))) - (( Im2 z2) * ( Im3 z1))) + (( Im3 z2) * ( Im2 z1))) / ( |.z2.| ^2 )), (((((( Rea z2) * ( Im2 z1)) + (( Im1 z2) * ( Im3 z1))) - (( Im2 z2) * ( Rea z1))) - (( Im3 z2) * ( Im1 z1))) / ( |.z2.| ^2 )), ( Im3 (z1 / z2))*] by QUATERN2: 30

 .= [*(((((( Rea z2) * ( Rea z1)) + (( Im1 z1) * ( Im1 z2))) + (( Im2 z2) * ( Im2 z1))) + (( Im3 z2) * ( Im3 z1))) / ( |.z2.| ^2 )), (((((( Rea z2) * ( Im1 z1)) - (( Im1 z2) * ( Rea z1))) - (( Im2 z2) * ( Im3 z1))) + (( Im3 z2) * ( Im2 z1))) / ( |.z2.| ^2 )), (((((( Rea z2) * ( Im2 z1)) + (( Im1 z2) * ( Im3 z1))) - (( Im2 z2) * ( Rea z1))) - (( Im3 z2) * ( Im1 z1))) / ( |.z2.| ^2 )), (((((( Rea z2) * ( Im3 z1)) - (( Im1 z2) * ( Im2 z1))) + (( Im2 z2) * ( Im1 z1))) - (( Im3 z2) * ( Rea z1))) / ( |.z2.| ^2 ))*] by QUATERN2: 30;

 hence thesis;

 end;

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



 Lm2: = [*( In ( 0 , REAL )), jj*] by ARYTM_0:def 5;

 theorem :: QUATERN3:75

 ( " ) = ( - )

 proof



 A1: ( Im3 ( " )) = ( - (( Im3 ) / ( |. .| ^2 ))) by QUATERN2: 29

 .= 0 by QUATERNI: 30;



 A2: ( Im2 ( " )) = ( - (( Im2 ) / ( |. .| ^2 ))) by QUATERN2: 29

 .= 0 by QUATERNI: 30;



 A3: ( Im1 ( " )) = ( - (( Im1 ) / ( |. .| ^2 ))) by QUATERN2: 29

 .= ( - 1) by QUATERNI: 30, QUATERNI: 69;

 ( Rea ( " )) = (( Rea ) / ( |. .| ^2 )) by QUATERN2: 29

 .= 0 by QUATERNI: 30;



 then ( " ) = [*( - 0 ), ( - 1), ( - 0 ), ( - 0 )*] by A3, A2, A1, QUATERNI: 24

 .= ( - [* 0 , jj, 0 , 0 *]) by QUATERN2: 4

 .= ( - ) by Lm2, QUATERNI:def 6;

 hence thesis;

 end;

 theorem :: QUATERN3:76

 ( <j> " ) = ( - <j> )

 proof



 A1: ( Im3 ( <j> " )) = ( - (( Im3 <j> ) / ( |. <j> .| ^2 ))) by QUATERN2: 29

 .= 0 by QUATERNI: 31;



 A2: ( Im2 ( <j> " )) = ( - (( Im2 <j> ) / ( |. <j> .| ^2 ))) by QUATERN2: 29

 .= ( - 1) by QUATERNI: 31, QUATERNI: 70;



 A3: ( Im1 ( <j> " )) = ( - (( Im1 <j> ) / ( |. <j> .| ^2 ))) by QUATERN2: 29

 .= 0 by QUATERNI: 31;

 ( Rea ( <j> " )) = (( Rea <j> ) / ( |. <j> .| ^2 )) by QUATERN2: 29

 .= 0 by QUATERNI: 31;



 then ( <j> " ) = [*( - 0 ), ( - 0 ), ( - jj), ( - 0 )*] by A3, A2, A1, QUATERNI: 24

 .= ( - <j> ) by QUATERN2: 4;

 hence thesis;

 end;

 theorem :: QUATERN3:77

 ( <k> " ) = ( - <k> )

 proof



 A1: ( Im3 ( <k> " )) = ( - (( Im3 <k> ) / ( |. <k> .| ^2 ))) by QUATERN2: 29

 .= ( - 1) by QUATERNI: 31, QUATERNI: 71;



 A2: ( Im2 ( <k> " )) = ( - (( Im2 <k> ) / ( |. <k> .| ^2 ))) by QUATERN2: 29

 .= 0 by QUATERNI: 31;



 A3: ( Im1 ( <k> " )) = ( - (( Im1 <k> ) / ( |. <k> .| ^2 ))) by QUATERN2: 29

 .= 0 by QUATERNI: 31;

 ( Rea ( <k> " )) = (( Rea <k> ) / ( |. <k> .| ^2 )) by QUATERN2: 29

 .= 0 by QUATERNI: 31;



 then ( <k> " ) = [*( - 0 ), ( - 0 ), ( - 0 ), ( - jj)*] by A3, A2, A1, QUATERNI: 24

 .= ( - <k> ) by QUATERN2: 4;

 hence thesis;

 end;

 definition

 let z be Quaternion;

 :: QUATERN3:def1

 func z ^2 -> Number equals (z * z);

 correctness ;

 end

 registration

 let z be Quaternion;

 cluster (z ^2 ) -> quaternion;

 coherence ;

 end

 definition

 let z be Element of QUATERNION ;

 :: original: ^2

 redefine

 func z ^2 -> Element of QUATERNION ;

 correctness ;

 end

 theorem :: QUATERN3:78



 Th78: (z ^2 ) = [*((((( Rea z) ^2 ) - (( Im1 z) ^2 )) - (( Im2 z) ^2 )) - (( Im3 z) ^2 )), (2 * (( Rea z) * ( Im1 z))), (2 * (( Rea z) * ( Im2 z))), (2 * (( Rea z) * ( Im3 z)))*]

 proof

 (z ^2 ) = [*( Rea (z ^2 )), ( Im1 (z ^2 )), ( Im2 (z ^2 )), ( Im3 (z ^2 ))*] by QUATERNI: 24

 .= [*((((( Rea z) ^2 ) - (( Im1 z) ^2 )) - (( Im2 z) ^2 )) - (( Im3 z) ^2 )), ( Im1 (z ^2 )), ( Im2 (z ^2 )), ( Im3 (z ^2 ))*] by QUATERNI: 40

 .= [*((((( Rea z) ^2 ) - (( Im1 z) ^2 )) - (( Im2 z) ^2 )) - (( Im3 z) ^2 )), (2 * (( Rea z) * ( Im1 z))), ( Im2 (z ^2 )), ( Im3 (z ^2 ))*] by QUATERNI: 40

 .= [*((((( Rea z) ^2 ) - (( Im1 z) ^2 )) - (( Im2 z) ^2 )) - (( Im3 z) ^2 )), (2 * (( Rea z) * ( Im1 z))), (2 * (( Rea z) * ( Im2 z))), ( Im3 (z ^2 ))*] by QUATERNI: 40

 .= [*((((( Rea z) ^2 ) - (( Im1 z) ^2 )) - (( Im2 z) ^2 )) - (( Im3 z) ^2 )), (2 * (( Rea z) * ( Im1 z))), (2 * (( Rea z) * ( Im2 z))), (2 * (( Rea z) * ( Im3 z)))*] by QUATERNI: 40;

 hence thesis;

 end;

 theorem :: QUATERN3:79

 ( 0q ^2 ) = 0

 proof



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

 .= [* 0 , 0 , 0 , 0 *] by QUATERNI: 91;

 then

 A2: ( Rea 0q ) = 0 & ( Im1 0q ) = 0 by QUATERNI: 23;



 A3: ( Im2 0q ) = 0 & ( Im3 0q ) = 0 by A1, QUATERNI: 23;

 ( 0q ^2 ) = [*((((( Rea 0q ) ^2 ) - (( Im1 0q ) ^2 )) - (( Im2 0q ) ^2 )) - (( Im3 0q ) ^2 )), (2 * (( Rea 0q ) * ( Im1 0q ))), (2 * (( Rea 0q ) * ( Im2 0q ))), (2 * (( Rea 0q ) * ( Im3 0q )))*] by Th78

 .= [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by A2, A3, QUATERNI: 91

 .= 0 by ARYTM_0:def 5;

 hence thesis;

 end;

 theorem :: QUATERN3:80

 ( 1q ^2 ) = 1

 proof



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

 .= [*jj, 0 , 0 , 0 *] by QUATERNI: 91;

 then

 A2: ( Rea 1q ) = 1 & ( Im1 1q ) = 0 by QUATERNI: 23;



 A3: ( Im2 1q ) = 0 & ( Im3 1q ) = 0 by A1, QUATERNI: 23;

 ( 1q ^2 ) = [*((((( Rea 1q ) ^2 ) - (( Im1 1q ) ^2 )) - (( Im2 1q ) ^2 )) - (( Im3 1q ) ^2 )), (2 * (( Rea 1q ) * ( Im1 1q ))), (2 * (( Rea 1q ) * ( Im2 1q ))), (2 * (( Rea 1q ) * ( Im3 1q )))*] by Th78

 .= [*jj, ( In ( 0 , REAL ))*] by A2, A3, QUATERNI: 91

 .= 1 by ARYTM_0:def 5;

 hence thesis;

 end;

 theorem :: QUATERN3:81



 Th81: (z ^2 ) = (( - z) ^2 )

 proof

 (( - z) ^2 ) = [*((((( Rea ( - z)) ^2 ) - (( Im1 ( - z)) ^2 )) - (( Im2 ( - z)) ^2 )) - (( Im3 ( - z)) ^2 )), (2 * (( Rea ( - z)) * ( Im1 ( - z)))), (2 * (( Rea ( - z)) * ( Im2 ( - z)))), (2 * (( Rea ( - z)) * ( Im3 ( - z))))*] by Th78

 .= [*((((( - ( Rea z)) ^2 ) - (( Im1 ( - z)) ^2 )) - (( Im2 ( - z)) ^2 )) - (( Im3 ( - z)) ^2 )), (2 * (( Rea ( - z)) * ( Im1 ( - z)))), (2 * (( Rea ( - z)) * ( Im2 ( - z)))), (2 * (( Rea ( - z)) * ( Im3 ( - z))))*] by QUATERNI: 41

 .= [*((((( - ( Rea z)) ^2 ) - (( - ( Im1 z)) ^2 )) - (( Im2 ( - z)) ^2 )) - (( Im3 ( - z)) ^2 )), (2 * (( Rea ( - z)) * ( Im1 ( - z)))), (2 * (( Rea ( - z)) * ( Im2 ( - z)))), (2 * (( Rea ( - z)) * ( Im3 ( - z))))*] by QUATERNI: 41

 .= [*((((( - ( Rea z)) ^2 ) - (( - ( Im1 z)) ^2 )) - (( - ( Im2 z)) ^2 )) - (( Im3 ( - z)) ^2 )), (2 * (( Rea ( - z)) * ( Im1 ( - z)))), (2 * (( Rea ( - z)) * ( Im2 ( - z)))), (2 * (( Rea ( - z)) * ( Im3 ( - z))))*] by QUATERNI: 41

 .= [*((((( - ( Rea z)) ^2 ) - (( - ( Im1 z)) ^2 )) - (( - ( Im2 z)) ^2 )) - (( - ( Im3 z)) ^2 )), (2 * (( Rea ( - z)) * ( Im1 ( - z)))), (2 * (( Rea ( - z)) * ( Im2 ( - z)))), (2 * (( Rea ( - z)) * ( Im3 ( - z))))*] by QUATERNI: 41

 .= [*((((( - ( Rea z)) ^2 ) - (( - ( Im1 z)) ^2 )) - (( - ( Im2 z)) ^2 )) - (( - ( Im3 z)) ^2 )), (2 * (( - ( Rea z)) * ( Im1 ( - z)))), (2 * (( Rea ( - z)) * ( Im2 ( - z)))), (2 * (( Rea ( - z)) * ( Im3 ( - z))))*] by QUATERNI: 41

 .= [*((((( - ( Rea z)) ^2 ) - (( - ( Im1 z)) ^2 )) - (( - ( Im2 z)) ^2 )) - (( - ( Im3 z)) ^2 )), (2 * (( - ( Rea z)) * ( - ( Im1 z)))), (2 * (( Rea ( - z)) * ( Im2 ( - z)))), (2 * (( Rea ( - z)) * ( Im3 ( - z))))*] by QUATERNI: 41

 .= [*((((( - ( Rea z)) ^2 ) - (( - ( Im1 z)) ^2 )) - (( - ( Im2 z)) ^2 )) - (( - ( Im3 z)) ^2 )), (2 * (( - ( Rea z)) * ( - ( Im1 z)))), (2 * (( - ( Rea z)) * ( Im2 ( - z)))), (2 * (( Rea ( - z)) * ( Im3 ( - z))))*] by QUATERNI: 41

 .= [*((((( - ( Rea z)) ^2 ) - (( - ( Im1 z)) ^2 )) - (( - ( Im2 z)) ^2 )) - (( - ( Im3 z)) ^2 )), (2 * (( - ( Rea z)) * ( - ( Im1 z)))), (2 * (( - ( Rea z)) * ( - ( Im2 z)))), (2 * (( Rea ( - z)) * ( Im3 ( - z))))*] by QUATERNI: 41

 .= [*((((( - ( Rea z)) ^2 ) - (( - ( Im1 z)) ^2 )) - (( - ( Im2 z)) ^2 )) - (( - ( Im3 z)) ^2 )), (2 * (( - ( Rea z)) * ( - ( Im1 z)))), (2 * (( - ( Rea z)) * ( - ( Im2 z)))), (2 * (( - ( Rea z)) * ( Im3 ( - z))))*] by QUATERNI: 41

 .= [*((((( - ( Rea z)) ^2 ) - (( - ( Im1 z)) ^2 )) - (( - ( Im2 z)) ^2 )) - (( - ( Im3 z)) ^2 )), (2 * (( - ( Rea z)) * ( - ( Im1 z)))), (2 * (( - ( Rea z)) * ( - ( Im2 z)))), (2 * (( - ( Rea z)) * ( - ( Im3 z))))*] by QUATERNI: 41

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

 hence thesis by Th78;

 end;

 definition

 let z be Quaternion;

 :: QUATERN3:def2

 func z ^3 -> Number equals ((z * z) * z);

 coherence ;

 end

 registration

 let z be Quaternion;

 cluster (z ^3 ) -> quaternion;

 coherence ;

 end

 definition

 let z be Element of QUATERNION ;

 :: original: ^3

 redefine

 func z ^3 -> Element of QUATERNION ;

 correctness ;

 end

 theorem :: QUATERN3:82

 ( 0q ^3 ) = 0

 proof



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

 .= [* 0 , 0 , 0 , 0 *] by QUATERNI: 91;

 then

 A2: ( Rea 0q ) = 0 & ( Im1 0q ) = 0 by QUATERNI: 23;



 A3: ( Im2 0q ) = 0 & ( Im3 0q ) = 0 by A1, QUATERNI: 23;

 ( 0q ^2 ) = [*((((( Rea 0q ) ^2 ) - (( Im1 0q ) ^2 )) - (( Im2 0q ) ^2 )) - (( Im3 0q ) ^2 )), (2 * (( Rea 0q ) * ( Im1 0q ))), (2 * (( Rea 0q ) * ( Im2 0q ))), (2 * (( Rea 0q ) * ( Im3 0q )))*] by Th78

 .= [*( In ( 0 , REAL )), ( In ( 0 , REAL ))*] by A2, A3, QUATERNI: 91

 .= 0 by ARYTM_0:def 5;

 hence thesis;

 end;

 theorem :: QUATERN3:83

 ( 1q ^3 ) = 1

 proof



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

 .= [*jj, 0 , 0 , 0 *] by QUATERNI: 91;

 then

 A2: ( Rea 1q ) = 1 & ( Im1 1q ) = 0 by QUATERNI: 23;



 A3: ( Im2 1q ) = 0 & ( Im3 1q ) = 0 by A1, QUATERNI: 23;

 ( 1q ^2 ) = [*((((( Rea 1q ) ^2 ) - (( Im1 1q ) ^2 )) - (( Im2 1q ) ^2 )) - (( Im3 1q ) ^2 )), (2 * (( Rea 1q ) * ( Im1 1q ))), (2 * (( Rea 1q ) * ( Im2 1q ))), (2 * (( Rea 1q ) * ( Im3 1q )))*] by Th78

 .= [*jj, ( In ( 0 , REAL ))*] by A2, A3, QUATERNI: 91

 .= 1 by ARYTM_0:def 5;

 hence thesis;

 end;

 theorem :: QUATERN3:84

 ( ^3 ) = ( - )

 proof

 = [* 0 , jj, 0 , 0 *] by Lm2, QUATERNI:def 6;



 then (( * ) * ) = ( [*(((( 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))*] * [* 0 , 1, 0 , 0 *]) by QUATERNI:def 10

 .= [*((((( - 1) * 0 ) - ( 0 * 1)) - ( 0 * 0 )) - ( 0 * 0 )), ((((( - 1) * 1) + ( 0 * 0 )) + ( 0 * 0 )) - ( 0 * 0 )), ((((( - 1) * 0 ) + ( 0 * 0 )) + (1 * 0 )) - ( 0 * 0 )), ((((( - 1) * 0 ) + ( 0 * 0 )) + ( 0 * 0 )) - ( 0 * jj))*] by QUATERNI:def 10

 .= ( - [* 0 , jj, 0 , 0 *]) by QUATERN2: 4;

 hence thesis by Lm2, QUATERNI:def 6;

 end;

 theorem :: QUATERN3:85

 ( <j> ^3 ) = ( - <j> )

 proof

 (( <j> * <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 ))*] * [* 0 , 0 , jj, 0 *]) by QUATERNI:def 10

 .= [*((((( - 1) * 0 ) - ( 0 * 0 )) - ( 0 * 1)) - ( 0 * 0 )), ((((( - 1) * 0 ) + ( 0 * 0 )) + ( 0 * 0 )) - ( 0 * 1)), ((((( - 1) * 1) + ( 0 * 0 )) + ( 0 * 0 )) - ( 0 * 0 )), ((((( - 1) * 0 ) + ( 0 * 0 )) + ( 0 * 1)) - ( 0 * 0 ))*] by QUATERNI:def 10

 .= ( - [* 0 , 0 , jj, 0 *]) by QUATERN2: 4;

 hence thesis;

 end;

 theorem :: QUATERN3:86

 ( <k> ^3 ) = ( - <k> )

 proof

 (( <k> * <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 ))*] * [* 0 , 0 , 0 , jj*]) by QUATERNI:def 10

 .= [*((((( - 1) * 0 ) - ( 0 * 0 )) - ( 0 * 0 )) - ( 0 * 1)), ((((( - 1) * 0 ) + ( 0 * 0 )) + ( 0 * 1)) - ( 0 * 0 )), ((((( - 1) * 0 ) + ( 0 * 0 )) + ( 0 * 0 )) - (1 * 0 )), ((((( - 1) * 1) + ( 0 * 0 )) + ( 0 * 0 )) - ( 0 * 0 ))*] by QUATERNI:def 10

 .= ( - [* 0 , 0 , 0 , jj*]) by QUATERN2: 4;

 hence thesis;

 end;

 theorem :: QUATERN3:87

 (( - 1q ) ^2 ) = 1

 proof

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

 .= [*jj, 0 , 0 , 0 *] by QUATERNI: 91;

 then

 A1: ( - 1q ) = [*( - jj), ( - 0 ), ( - 0 ), ( - 0 )*] by QUATERN2: 4;

 then

 A2: ( Rea ( - 1q )) = ( - 1) & ( Im1 ( - 1q )) = 0 by QUATERNI: 23;



 A3: ( Im2 ( - 1q )) = 0 & ( Im3 ( - 1q )) = 0 by A1, QUATERNI: 23;

 (( - 1q ) ^2 ) = [*((((( Rea ( - 1q )) ^2 ) - (( Im1 ( - 1q )) ^2 )) - (( Im2 ( - 1q )) ^2 )) - (( Im3 ( - 1q )) ^2 )), (2 * (( Rea ( - 1q )) * ( Im1 ( - 1q )))), (2 * (( Rea ( - 1q )) * ( Im2 ( - 1q )))), (2 * (( Rea ( - 1q )) * ( Im3 ( - 1q ))))*] by Th78

 .= [*jj, ( In ( 0 , REAL ))*] by A2, A3, QUATERNI: 91

 .= 1 by ARYTM_0:def 5;

 hence thesis;

 end;

 theorem :: QUATERN3:88

 (( - 1q ) ^3 ) = ( - 1)

 proof



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

 .= [*1, 0 , 0 , 0 *] by QUATERNI: 91;

 then

 A2: ( - 1q ) = [*( - jj), ( - 0 ), ( - 0 ), ( - 0 )*] by QUATERN2: 4;

 then

 A3: ( Rea ( - 1q )) = ( - 1) & ( Im1 ( - 1q )) = 0 by QUATERNI: 23;



 A4: ( Im2 ( - 1q )) = 0 & ( Im3 ( - 1q )) = 0 by A2, QUATERNI: 23;

 (( - 1q ) ^2 ) = [*((((( Rea ( - 1q )) ^2 ) - (( Im1 ( - 1q )) ^2 )) - (( Im2 ( - 1q )) ^2 )) - (( Im3 ( - 1q )) ^2 )), (2 * (( Rea ( - 1q )) * ( Im1 ( - 1q )))), (2 * (( Rea ( - 1q )) * ( Im2 ( - 1q )))), (2 * (( Rea ( - 1q )) * ( Im3 ( - 1q ))))*] by Th78

 .= [*jj, ( In ( 0 , REAL ))*] by A3, A4, QUATERNI: 91

 .= 1 by ARYTM_0:def 5;



 then (( - 1q ) ^3 ) = ( - 1q ) by QUATERN2: 15

 .= [*( - jj), ( - 0 ), ( - 0 ), ( - 0 )*] by A1, QUATERN2: 4

 .= [*( - jj), ( - ( In ( 0 , REAL )))*] by QUATERNI: 91

 .= ( - 1) by ARYTM_0:def 5;

 hence thesis;

 end;

 theorem :: QUATERN3:89

 (z ^3 ) = ( - (( - z) ^3 ))

 proof



 A1: (z ^3 ) = (z * (z ^2 )) by QUATERN2: 16;

 (( - z) ^3 ) = (( - z) * (( - z) ^2 )) by QUATERN2: 16

 .= (( - z) * (z ^2 )) by Th81

 .= ((( - 1q ) * z) * (z ^2 )) by QUATERN2: 19

 .= (( - 1q ) * (z * (z ^2 ))) by QUATERN2: 16

 .= ( - (z ^3 )) by A1, QUATERN2: 19;

 hence thesis;

 end;