A --> 0c is Function of A,COMPLEX ;
hence A --> 0 is Element of Funcs A,COMPLEX by FUNCT_2:11; :: thesis: verum