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 --> {0});
consider A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) such that
A2: Free (S,X) = GenMSAlg A and
A3: A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X by Def1;
A is MSSubset of (Free (S,X)) by A2, MSUALG_2:def 17;
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 --> {0}) by PBOOLE:14;
then X . s c= (X (\/) ( the carrier of S --> {0})) . 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