deffunc H_{1}( 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_{1}(s)
from PBOOLE:sch 5();

T c= the Sorts of (FreeMSA Y)

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

consider T being ManySortedSet of the carrier of S such that

A1: for s being SortSymbol of S holds T . s = H

T c= the Sorts of (FreeMSA Y)

proof

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

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