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

proof

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

end;

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