defpred S₁[ Element of COMPLEX , set ] means $2 = F₁($1);
A1: for x being Element of COMPLEX ex y being Element of COMPLEX st S₁[x,y]

proof

let x be Element of COMPLEX ; :: thesis: ex y being Element of COMPLEX st S₁[x,y]
reconsider y = F₁(x) as Element of COMPLEX by XCMPLX_0:def 2;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider f being Function of COMPLEX,COMPLEX such that
A2: for x being Element of COMPLEX holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for x being complex number holds f . x = F₁(x)
let c be complex number ; :: thesis: f . c = F₁(c)
reconsider c = c as Element of COMPLEX by XCMPLX_0:def 2;
S₁[c,f . c] by A2;
hence f . c = F₁(c) ; :: thesis: verum