begin
Lm1:
for x, y, z being quaternion number st z = x * y holds
( Rea z = ((((Rea x) * (Rea y)) - ((Im1 x) * (Im1 y))) - ((Im2 x) * (Im2 y))) - ((Im3 x) * (Im3 y)) & Im1 z = ((((Rea x) * (Im1 y)) + ((Im1 x) * (Rea y))) + ((Im2 x) * (Im3 y))) - ((Im3 x) * (Im2 y)) & Im2 z = ((((Rea x) * (Im2 y)) + ((Im2 x) * (Rea y))) + ((Im3 x) * (Im1 y))) - ((Im1 x) * (Im3 y)) & Im3 z = ((((Rea x) * (Im3 y)) + ((Im3 x) * (Rea y))) + ((Im1 x) * (Im2 y))) - ((Im2 x) * (Im1 y)) )
theorem Th1:
Lm2:
for z being quaternion number st z is Real holds
( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th11:
theorem
theorem
theorem
theorem
theorem
theorem Th17:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th36:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem
theorem Th61:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th74:
theorem
theorem
theorem
theorem
Lm3:
<i> = [*0 ,1*]
by ARYTM_0:def 7;
theorem
theorem
theorem
:: deftheorem defines ^2 QUATERN3:def 1 :
for z being quaternion number holds z ^2 = z * z;
theorem Th82:
theorem
theorem
theorem Th85:
:: deftheorem defines ^3 QUATERN3:def 2 :
for z being quaternion number holds z ^3 = (z * z) * z;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem