let x be set ; :: according to VALUED_0:def 7 :: thesis: ( not x in proj1 (f ^ ) or (f ^ ) . x is complex )
set F = f ^ ;
assume x in dom (f ^ ) ; :: thesis: (f ^ ) . x is complex
then (f ^ ) . x = (f . x) " by Def8;
hence (f ^ ) . x is complex ; :: thesis: verum