let S be non void Signature; :: thesis: for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S holds () "" X c= S -Terms (X,Y)

let Y be V8() ManySortedSet of the carrier of S; :: thesis: for X being ManySortedSet of the carrier of S holds () "" X c= S -Terms (X,Y)
let X be ManySortedSet of the carrier of S; :: thesis: () "" X c= S -Terms (X,Y)
let s be object ; :: according to PBOOLE:def 2 :: thesis: ( not s in the carrier of S or (() "" X) . s c= (S -Terms (X,Y)) . s )
assume s in the carrier of S ; :: thesis: (() "" X) . s c= (S -Terms (X,Y)) . s
then reconsider s9 = s as SortSymbol of S ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (() "" X) . s or x in (S -Terms (X,Y)) . s )
assume x in (() "" X) . s ; :: thesis: x in (S -Terms (X,Y)) . s
then A1: x in (() . s9) " (X . s9) by EQUATION:def 1;
then A2: x in dom (() . s) by FUNCT_1:def 7;
A3: ((Reverse Y) . s) . x in X . s by ;
A4: (Reverse Y) . s = Reverse (s9,Y) by MSAFREE:def 18;
then A5: dom (() . s) = FreeGen (s9,Y) by FUNCT_2:def 1;
then consider b being set such that
A6: b in Y . s9 and
A7: x = root-tree [b,s9] by ;
FreeGen (s9,Y) = { () where t is Symbol of () : ( t in Terminals () & t `2 = s ) } by MSAFREE:13;
then consider a being Symbol of () such that
A8: x = root-tree a and
a in Terminals () and
a `2 = s by A2, A5;
(Reverse (s9,Y)) . x = a `1 by
.= [b,s] `1 by
.= b ;
hence x in (S -Terms (X,Y)) . s by A3, A4, A6, A7, Th18; :: thesis: verum