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

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