let S be non void Signature; :: thesis: for X being V5() 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 V5() 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 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