let x be set ; :: thesis: for S being non void Signature
for X being ManySortedSet of
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
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 ; :: 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 & A = (Reverse (X \/ (the carrier of S --> {0 }))) "" X ) by Def2;
( A is MSSubset of (Free S,X) & X c= X \/ (the carrier of S --> {0 }) ) by A2, MSUALG_2:def 18, PBOOLE:16;
then ( A c= the Sorts of (Free S,X) & X . s c= (X \/ (the carrier of S --> {0 })) . s ) by PBOOLE:def 5, PBOOLE:def 23;
then ( root-tree [x,s] in A . s & A . s c= the Sorts of (Free S,X) . s ) by A1, A2, Th4, PBOOLE:def 5;
hence root-tree [x,s] in the Sorts of (Free S,X) . s ; :: thesis: verum