consider t being Element of the Sorts of (Free C,(MSVars C)) . s;
dom the Sorts of (Free C,(MSVars C)) = the carrier of C by PARTFUN1:def 4;
then t in Union the Sorts of (Free C,(MSVars C)) by CARD_5:10;
hence ex b₁ being expression of C st b₁ in the Sorts of (Free C,(MSVars C)) . s ; :: thesis: verum