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;