let S be non void Signature; :: thesis: for Y being V5() ManySortedSet of
for X being ManySortedSet of holds (Reverse Y) "" X c= S -Terms X,Y
let Y be V5() ManySortedSet of ; :: thesis: for X being ManySortedSet of holds (Reverse Y) "" X c= S -Terms X,Y
let X be ManySortedSet of ; :: thesis: (Reverse Y) "" X c= S -Terms X,Y
let s be set ; :: according to PBOOLE:def 5 :: 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 s' = s as SortSymbol of S ;
let x be set ; :: 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 x in ((Reverse Y) . s') " (X . s') by EQUATION:def 1;
then A1: ( x in dom ((Reverse Y) . s) & ((Reverse Y) . s) . x in X . s ) by FUNCT_1:def 13;
A2: (Reverse Y) . s = Reverse s',Y by MSAFREE:def 20;
then A3: dom ((Reverse Y) . s) = FreeGen s',Y by FUNCT_2:def 1;
FreeGen s',Y = { (root-tree t) where t is Symbol of (DTConMSA Y) : ( t in Terminals (DTConMSA Y) & t `2 = s ) } by MSAFREE:14;
then consider a being Symbol of (DTConMSA Y) such that
A4: ( x = root-tree a & a in Terminals (DTConMSA Y) & a `2 = s ) by A1, A3;
consider b being set such that
A5: ( b in Y . s' & x = root-tree [b,s'] ) by A1, A3, MSAFREE:def 17;
(Reverse s',Y) . x = a `1 by A1, A3, A4, MSAFREE:def 19
.= [b,s] `1 by A4, A5, TREES_4:4
.= b by MCART_1:7 ;
hence x in (S -Terms X,Y) . s by A1, A2, A5, Th19; :: thesis: verum