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

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 V8() 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