:: deftheorem Def2 defines Im COMPLEX1:def 2 :
for z being Complex
for b₂ being number holds
( ( z is real implies ( b₂ = Im z iff b₂ = 0 ) ) & ( not z is real implies ( b₂ = Im z iff ex f being Function of 2,REAL st
( z = f & b₂ = f . 1 ) ) ) );