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

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