let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S

for v being SortSymbol of S

for e being Element of the Sorts of (FreeMSA X) . v holds e is finite DecoratedTree

let X be V5() ManySortedSet of the carrier of S; :: thesis: for v being SortSymbol of S

for e being Element of the Sorts of (FreeMSA X) . v holds e is finite DecoratedTree

let v be SortSymbol of S; :: thesis: for e being Element of the Sorts of (FreeMSA X) . v holds e is finite DecoratedTree

let e be Element of the Sorts of (FreeMSA X) . v; :: thesis: e is finite DecoratedTree

FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 14;

then the Sorts of (FreeMSA X) . v = FreeSort (X,v) by MSAFREE:def 11;

then A1: e in TS (DTConMSA X) by TARSKI:def 3;

then reconsider e9 = e as DecoratedTree ;

dom e9 is finite by A1;

hence e is finite DecoratedTree by FINSET_1:10; :: thesis: verum

for v being SortSymbol of S

for e being Element of the Sorts of (FreeMSA X) . v holds e is finite DecoratedTree

let X be V5() ManySortedSet of the carrier of S; :: thesis: for v being SortSymbol of S

for e being Element of the Sorts of (FreeMSA X) . v holds e is finite DecoratedTree

let v be SortSymbol of S; :: thesis: for e being Element of the Sorts of (FreeMSA X) . v holds e is finite DecoratedTree

let e be Element of the Sorts of (FreeMSA X) . v; :: thesis: e is finite DecoratedTree

FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 14;

then the Sorts of (FreeMSA X) . v = FreeSort (X,v) by MSAFREE:def 11;

then A1: e in TS (DTConMSA X) by TARSKI:def 3;

then reconsider e9 = e as DecoratedTree ;

dom e9 is finite by A1;

hence e is finite DecoratedTree by FINSET_1:10; :: thesis: verum