canonical_homomorphism T is_homomorphism Free (S,X),T by MSAFREE4:def 10;
hence canonical_homomorphism T is Homomorphism of Free (S,X),T by HOMO; :: thesis: verum