defpred S₁[ set , set ] means for z being Complex st z = $1 holds
$2 = z + 1;
A1: for x being Element of COMPLEX ex zz being Element of COMPLEX st S₁[x,zz]

proof

let x be Element of COMPLEX ; :: thesis: ex zz being Element of COMPLEX st S₁[x,zz]
reconsider z0 = x as Complex ;
reconsider z1 = z0 + 1 as Element of COMPLEX by XCMPLX_0:def 2;
take z1 ; :: thesis: S₁[x,z1]
thus S₁[x,z1] ; :: 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 z being Complex holds f . z = z + 1

now :: thesis: for z being Complex holds f . z = z + 1

let z be Complex; :: thesis: f . z = z + 1
reconsider zz = z as Element of COMPLEX by XCMPLX_0:def 2;
( z = zz & S₁[zz,f . zz] ) by A2;
hence f . z = z + 1 ; :: thesis: verum

end;

hence for z being Complex holds f . z = z + 1 ; :: thesis: verum