s is ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
then s . (the_array_sort_of S) is Function of ( the generators of G . (the_array_sort_of S)),( the Sorts of C . (the_array_sort_of S)) by PBOOLE:def 15;
then A1: (s . (the_array_sort_of S)) . M in the Sorts of C . (the_array_sort_of S) by FUNCT_2:5;
the Sorts of C . (the_array_sort_of S) = INT ^omega by Th74;
hence ( (s . (the_array_sort_of S)) . M is finite & (s . (the_array_sort_of S)) . M is Sequence-like & (s . (the_array_sort_of S)) . M is INT -valued ) by A1; :: thesis: verum