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

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