set t = the 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 2;
then the Element of the Sorts of (Free (C,(MSVars C))) . s in Union the Sorts of (Free (C,(MSVars C))) by CARD_5:2;
hence ex b₁ being expression of C st b₁ in the Sorts of (Free (C,(MSVars C))) . s ; :: thesis: verum