( the Sorts of C . I = INT & s is ManySortedFunction of the generators of G, the Sorts of C ) by AOFA_A00:48, AOFA_A00:55;
then s . I is Function of ( the generators of G . I),INT by PBOOLE:def 15;
then (s . I) . x in INT by FUNCT_2:5;
hence (s . I) . x is integer ; :: thesis: verum