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

suppose z in REAL ; :: thesis: Im z is real

hence Im z is real by Def3; :: thesis: verum

end;

suppose not z in REAL ; :: thesis: Im z is real

then consider f being Function of 2,REAL such that
z = f and
A2: Im z = f . 1 by Def3;
1 in 2 by CARD_1:88, TARSKI:def 2;
then f . 1 in REAL by FUNCT_2:7;
hence Im z is real by A2; :: thesis: verum

end;

end;