let S be non void Signature; :: thesis: for Y being non-empty ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S holds (Reverse Y) "" X c= S -Terms (X,Y)
let Y be non-empty ManySortedSet of the carrier of S; :: thesis: for X being ManySortedSet of the carrier of S holds (Reverse Y) "" X c= S -Terms (X,Y)
let X be ManySortedSet of the carrier of S; :: thesis: (Reverse Y) "" X c= S -Terms (X,Y)
let s be object ; :: according to PBOOLE:def 2 :: thesis: ( not s in the carrier of S or ((Reverse Y) "" X) . s c= (S -Terms (X,Y)) . s )
assume s in the carrier of S ; :: thesis: ((Reverse Y) "" 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 ((Reverse Y) "" X) . s or x in (S -Terms (X,Y)) . s )
assume x in ((Reverse Y) "" X) . s ; :: thesis: x in (S -Terms (X,Y)) . s
then A1: x in ((Reverse Y) . s9) " (X . s9) by EQUATION:def 1;
then A2: x in dom ((Reverse Y) . s) by FUNCT_1:def 7;
A3: ((Reverse Y) . s) . x in X . s by A1, FUNCT_1:def 7;
A4: (Reverse Y) . s = Reverse (s9,Y) by MSAFREE:def 18;
then A5: dom ((Reverse Y) . 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 A2, MSAFREE:def 15;
FreeGen (s9,Y) = { (root-tree t) where t is Symbol of (DTConMSA Y) : ( t in Terminals (DTConMSA Y) & t `2 = s ) } by MSAFREE:13;
then consider a being Symbol of (DTConMSA Y) such that
A8: x = root-tree a and
a in Terminals (DTConMSA Y) and
a `2 = s by A2, A5;
(Reverse (s9,Y)) . x = a `1 by A2, A5, A8, MSAFREE:def 17
.= [b,s] `1 by A8, A7, TREES_4:4
.= b ;
hence x in (S -Terms (X,Y)) . s by A3, A4, A6, A7, Th18; :: thesis: verum