let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of
for v being SortSymbol of
for e being Element of the Sorts of (FreeMSA X) . v holds e is finite DecoratedTree
let X be V5() ManySortedSet of ; :: thesis: for v being SortSymbol of
for e being Element of the Sorts of (FreeMSA X) . v holds e is finite DecoratedTree
let v be SortSymbol of ; :: 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 16;
then the Sorts of (FreeMSA X) . v = FreeSort X,v by MSAFREE:def 13;
then A1: e in TS (DTConMSA X) by TARSKI:def 3;
then reconsider e' = e as DecoratedTree by TREES_3:def 6;
dom e' is finite by A1;
hence e is finite DecoratedTree by FINSET_1:29; :: thesis: verum