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 (Reverse Y) "" 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 (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

for X being ManySortedSet of the carrier of S holds (Reverse Y) "" 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 (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