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 Def2;
A is MSSubset of (Free S,X) by A2, MSUALG_2:def 18;
then A c= the Sorts of (Free S,X) by PBOOLE:def 23;
then A4: A . s c= the Sorts of (Free S,X) . s by PBOOLE:def 5;
X c= X \/ (the carrier of S --> {0 }) by PBOOLE:16;
then X . s c= (X \/ (the carrier of S --> {0 })) . s by PBOOLE:def 5;
then root-tree [x,s] in A . s by A1, A3, Th4;
hence root-tree [x,s] in the Sorts of (Free S,X) . s by A4; :: thesis: verum