let S be positive Nat; :: thesis: { f where f is Solution_of_Sierp168 of S : verum } is infinite
set F = Solutions_of_Sierp168 the Solution_of_Sierp168 of S;
A1: dom (Solutions_of_Sierp168 the Solution_of_Sierp168 of S) = NATPLUS by PARTFUN1:def 2;
rng (Solutions_of_Sierp168 the Solution_of_Sierp168 of S) c= { f where f is Solution_of_Sierp168 of S : verum } by Th72;
hence { f where f is Solution_of_Sierp168 of S : verum } is infinite by A1, CARD_1:59; :: thesis: verum