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

suppose z is real ; :: thesis: Re z is real

hence Re z is real by Def1; :: thesis: verum

end;

suppose not z is real ; :: thesis: Re z is real

then consider f being Function of 2,REAL such that
z = f and
A1: Re z = f . 0 by Def1;
0 in 2 by CARD_1:50, TARSKI:def 2;
then f . 0 in REAL by FUNCT_2:5;
hence Re z is real by A1; :: thesis: verum

end;

end;