let S be non void Signature; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for s being SortSymbol of S
for x being Term of S,X holds
( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for s being SortSymbol of S
for x being Term of S,X holds
( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s )
let s be SortSymbol of S; :: thesis: for x being Term of S,X holds
( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s )
FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 14;
then the Sorts of (FreeMSA X) . s = FreeSort (X,s) by MSAFREE:def 11;
hence for x being Term of S,X holds
( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s ) by MSATERM:def 5; :: thesis: verum