card S is finite ;
then card (the_Target_of S) is finite by Th7, FINSET_1:1;
hence the_Target_of S is finite ; :: thesis: verum