begin
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 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