c in X ^omega by AFINSQ_1:def 8;
hence f . c is Element of X by FUNCT_2:7; :: thesis: verum