per cases ( z in COMPLEX or not z in COMPLEX ) ;
suppose z in COMPLEX ; :: thesis: Im3 z is real
hence Im3 z is real by Def15; :: thesis: verum
end;
suppose not z in COMPLEX ; :: thesis: Im3 z is real
then ex f being Function of 4,REAL st
( z = f & Im3 z = f . 3 ) by Def15;
hence Im3 z is real ; :: thesis: verum
end;
end;