:: deftheorem Def15 defines Im3 QUATERNI:def 15 :
for z being Quaternion
for b₂ being Number holds
( ( z in COMPLEX implies ( b₂ = Im3 z iff b₂ = 0 ) ) & ( not z in COMPLEX implies ( b₂ = Im3 z iff ex f being Function of 4,REAL st
( z = f & b₂ = f . 3 ) ) ) );