dom f = X by FUNCT_2:def 1;
then support f c= X by Th36;
hence support f is Element of Fin X by FINSUB_1:def 5; :: thesis: verum