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 the carrier of S 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 object ; :: according to PBOOLE:def 2 :: 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 s9 = s as SortSymbol of S ;
let x be object ; :: 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 . s9 = { t where t is Term of S,Y : ( the_sort_of t = s9 & variables_in t c= X ) } by A1;
then ex t being Term of S,Y st
( x = t & the_sort_of t = s9 & variables_in t c= X ) by A2;
hence x in the Sorts of (FreeMSA Y) . s by Th7; :: thesis: verum

end;

then reconsider T = T as MSSubset of (FreeMSA Y) by PBOOLE:def 18;
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