reconsider c = c as Element of COMPLEX by XCMPLX_0:def 2;
f /. c = f . c by FUNCT_2:99;
hence f /. c = f . c ; :: thesis: verum