:: deftheorem Def13 defines Im1 QUATERNI:def 13 :
for z being Quaternion
for b₂ being Number holds
( ( z in COMPLEX implies ( b₂ = Im1 z iff ex z9 being Complex st
( z = z9 & b₂ = Im z9 ) ) ) & ( not z in COMPLEX implies ( b₂ = Im1 z iff ex f being Function of 4,REAL st
( z = f & b₂ = f . 1 ) ) ) );