reconsider s = s as ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
the Sorts of C . the bool-sort of S = BOOLEAN by AOFA_A00:def 32;
then (s . the bool-sort of S) . b in BOOLEAN ;
hence (s . the bool-sort of S) . b is boolean ; :: thesis: verum