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