let f be Y -valued Function; :: thesis: f is complex-functions-valued
rng f c= Y by RELAT_1:def 19;
hence rng f is complex-functions-membered ; :: according to VALUED_2:def 20 :: thesis: verum