deffunc H₁( SortSymbol of ) -> set = { t where t is Term of the carrier of (DTConMSA Y), : ( the_sort_of t = $1 & variables_in t c= X ) } ;
consider T being ManySortedSet of the carrier of S such that
A1: for s being SortSymbol of holds T . s = H₁(s) from PBOOLE:sch 5();
T c= the Sorts of (FreeMSA Y)

proof

let s be set ; :: according to PBOOLE:def 5 :: thesis: ( not s in the carrier of S or T . s c= the Sorts of (FreeMSA Y) . s )
assume s in the carrier of S ; :: thesis: T . s c= the Sorts of (FreeMSA Y) . s
then reconsider s' = s as SortSymbol of ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in T . s or x in the Sorts of (FreeMSA Y) . s )
assume A2: x in T . s ; :: thesis: x in the Sorts of (FreeMSA Y) . s
T . s' = { t where t is Term of the carrier of (DTConMSA Y), : ( the_sort_of t = s' & variables_in t c= X ) } by A1;
then ex t being Term of the carrier of (DTConMSA Y), st
( x = t & the_sort_of t = s' & variables_in t c= X ) by A2;
hence x in the Sorts of (FreeMSA Y) . s by Th8; :: thesis: verum

end;

then reconsider T = T as MSSubset of by PBOOLE:def 23;
take T ; :: thesis: for s being SortSymbol of holds T . s = { t where t is Term of the carrier of (DTConMSA Y), : ( the_sort_of t = s & variables_in t c= X ) }
thus for s being SortSymbol of holds T . s = { t where t is Term of the carrier of (DTConMSA Y), : ( the_sort_of t = s & variables_in t c= X ) } by A1; :: thesis: verum