per cases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; :: thesis: f . x is complex-valued
then f . x in rng f by FUNCT_1:def 3;
hence f . x is complex-valued ; :: thesis: verum
end;
suppose not x in dom f ; :: thesis: f . x is complex-valued
hence f . x is complex-valued by FUNCT_1:def 2; :: thesis: verum
end;
end;