let f be Y -valued Function; :: thesis: f is complex-functions-valued
thus rng f is complex-functions-membered ; :: according to VALUED_2:def 20 :: thesis: verum