A1: dom f = A by FUNCT_2:def 1;
rng f c= COMPLEX by NUMBERS:11;
then f is Function of A,COMPLEX by A1, FUNCT_2:2;
hence - f is finite-support ; :: thesis: verum