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

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

hence Im2 z is real by Def15; :: thesis: verum

end;

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

then consider f being Function of 4, REAL such that
z = f and
A5: Im2 z = f . 2 by Def15;
thus Im2 z is real by A5; :: thesis: verum

end;

end;