take 0. F_Complex ; :: thesis: ( 0. F_Complex is real & 0. F_Complex is imaginary )
thus ( 0. F_Complex is real & 0. F_Complex is imaginary ) ; :: thesis: verum