defpred S₁[ set ] means $1 is finite ;
{ p where p is Element of sproduct (the_Values_of S) : S₁[p] } c= sproduct (the_Values_of S) from FRAENKEL:sch 10();
hence { p where p is Element of sproduct (the_Values_of S) : p is finite } is Subset of (sproduct (the_Values_of S)) ; :: thesis: verum