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;
thus ( (s . (the_array_sort_of S)) . M is Function-like & (s . (the_array_sort_of S)) . M is Relation-like ) by A1; :: thesis: verum