consider h being ManySortedFunction of T,C such that
A1: h is_epimorphism T,C by MSAFREE4:def 5;
h is_homomorphism T,C by A1, MSUALG_3:def 8;
then h || X in C -States X by Def18;
hence not C -States X is empty ; :: thesis: verum