let f be Function; :: thesis: ( f is complex-valued iff for x being set holds f . x is complex )

hereby :: thesis: ( ( for x being set holds f . x is complex ) implies f is complex-valued )

assume A1: f is complex-valued ; :: thesis: for x being set holds f . b₂ is complex
let x be set ; :: thesis: f . b₁ is complex

per cases ( x in dom f or not x in dom f ) ;

suppose x in dom f ; :: thesis: f . b₁ is complex

hence f . x is complex by A1, Def7; :: thesis: verum

end;

suppose not x in dom f ; :: thesis: f . b₁ is complex

hence f . x is complex by FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

assume for x being set holds f . x is complex ; :: thesis: f is complex-valued
then for x being set st x in dom f holds
f . x is complex ;
hence f is complex-valued by Def7; :: thesis: verum