let S be non void Signature; :: thesis: for X being V5() ManySortedSet of
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 V5() ManySortedSet of ; :: 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 16;
then the Sorts of (FreeMSA X) . s = FreeSort X,s by MSAFREE:def 13;
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