deffunc H₁( SortSymbol of S) -> set = { t where t is Term of S,Y : ( the_sort_of t = $1 & variables_in t c= X ) } ;
consider T being ManySortedSet of such that
A1: for s being SortSymbol of S 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 S ;
A2: T . s' = { t where t is Term of S,Y : ( the_sort_of t = s' & variables_in t c= X ) } by A1;
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 x in T . s ; :: thesis: x in the Sorts of (FreeMSA Y) . s
then ex t being Term of S,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 (FreeMSA Y) by PBOOLE:def 23;
take T ; :: thesis: for s being SortSymbol of S holds T . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) }
thus for s being SortSymbol of S holds T . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } by A1; :: thesis: verum