set G = the free GeneratorSet of T;
set f = the ManySortedFunction of the free GeneratorSet of T, the Sorts of C;
consider h being ManySortedFunction of T,C such that
A1: ( h is_homomorphism T,C & h || the free GeneratorSet of T = the ManySortedFunction of the free GeneratorSet of T, the Sorts of C ) by MSAFREE:def 5;
h || X in C -States X by A1, Def18;
hence not C -States X is empty ; :: thesis: verum