per cases ( z in COMPLEX or not z in COMPLEX ) ;

suppose z in COMPLEX ; :: thesis: Im3 z is real

hence Im3 z is real by Def16; :: thesis: verum

end;

suppose not z in COMPLEX ; :: thesis: Im3 z is real

then consider f being Function of 4, REAL such that
z = f and
A6: Im3 z = f . 3 by Def16;
thus Im3 z is real by A6; :: thesis: verum

end;

end;