{x,y} is Subset of X by SUBSET_1:34;
hence {.y,.} is Element of Fin X by FINSUB_1:def 5; :: thesis: verum