per cases ( z is real or not z is real ) ;

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

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

end;

suppose not z is 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 Def2;
1 in 2 by CARD_1:50, TARSKI:def 2;
then f . 1 in REAL by FUNCT_2:5;
hence Im z is real by A2; :: thesis: verum

end;

end;