let x be set ; :: thesis: for S being non void Signature
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S st x in X . s holds
root-tree [x,s] in the Sorts of (Free (S,X)) . s

let S be non void Signature; :: thesis: for X being ManySortedSet of the carrier of S
for s being SortSymbol of S st x in X . s holds
root-tree [x,s] in the Sorts of (Free (S,X)) . s

let X be ManySortedSet of the carrier of S; :: thesis: for s being SortSymbol of S st x in X . s holds
root-tree [x,s] in the Sorts of (Free (S,X)) . s

let s be SortSymbol of S; :: thesis: ( x in X . s implies root-tree [x,s] in the Sorts of (Free (S,X)) . s )
assume A1: x in X . s ; :: thesis: root-tree [x,s] in the Sorts of (Free (S,X)) . s
set Y = X (\/) ( the carrier of S --> );
consider A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> ))) such that
A2: Free (S,X) = GenMSAlg A and
A3: A = (Reverse (X (\/) ( the carrier of S --> ))) "" X by Def1;
A is MSSubset of (Free (S,X)) by ;
then A c= the Sorts of (Free (S,X)) by PBOOLE:def 18;
then A4: A . s c= the Sorts of (Free (S,X)) . s ;
X c= X (\/) ( the carrier of S --> ) by PBOOLE:14;
then X . s c= (X (\/) ( the carrier of S --> )) . s ;
then root-tree [x,s] in A . s by A1, A3, Th3;
hence root-tree [x,s] in the Sorts of (Free (S,X)) . s by A4; :: thesis: verum