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