for x being object st x in COMPLEX * holds
x is complex-valued Function ;
hence COMPLEX * is complex-functions-membered by VALUED_2:def 2; :: thesis: verum