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

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

then consider z' being complex number such that
z = z' and
A3: Im1 z = Im z' by Def14;
thus Im1 z is real by A3; :: thesis: verum

end;

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

then consider f being Function of 4, REAL such that
z = f and
A4: Im1 z = f . 1 by Def14;
thus Im1 z is real by A4; :: thesis: verum

end;

end;