let x be set ; :: thesis: for S being non void Signature

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S

for s being SortSymbol of S holds

( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )

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

for s being SortSymbol of S holds

( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )

let Y be V8() ManySortedSet of the carrier of S; :: thesis: for X being ManySortedSet of the carrier of S

for s being SortSymbol of S holds

( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )

let X be ManySortedSet of the carrier of S; :: thesis: for s being SortSymbol of S holds

( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )

let s be SortSymbol of S; :: thesis: ( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )

A1: (Reverse Y) . s = Reverse (s,Y) by MSAFREE:def 18;

A2: dom (Reverse (s,Y)) = FreeGen (s,Y) by FUNCT_2:def 1;

then A6: root-tree [x,s] in ((Reverse Y) . s) " (X . s) by EQUATION:def 1;

then A7: (Reverse (s,Y)) . (root-tree [x,s]) in X . s by A1, FUNCT_1:def 7;

A8: root-tree [x,s] in FreeGen (s,Y) by A1, A2, A6, FUNCT_1:def 7;

then consider z being set such that

A9: z in Y . s and

A10: root-tree [x,s] = root-tree [z,s] by MSAFREE:def 15;

B: [z,s] `1 = z ;

A11: [x,s] = [z,s] by A10, TREES_4:4;

then [x,s] in the carrier of (DTConMSA Y) by A9, Th2;

then [x,s] `1 in X . s by A8, A7, MSAFREE:def 17;

hence ( x in X . s & x in Y . s ) by A9, A11, B; :: thesis: verum

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S

for s being SortSymbol of S holds

( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )

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

for s being SortSymbol of S holds

( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )

let Y be V8() ManySortedSet of the carrier of S; :: thesis: for X being ManySortedSet of the carrier of S

for s being SortSymbol of S holds

( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )

let X be ManySortedSet of the carrier of S; :: thesis: for s being SortSymbol of S holds

( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )

let s be SortSymbol of S; :: thesis: ( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )

A1: (Reverse Y) . s = Reverse (s,Y) by MSAFREE:def 18;

A2: dom (Reverse (s,Y)) = FreeGen (s,Y) by FUNCT_2:def 1;

hereby :: thesis: ( root-tree [x,s] in ((Reverse Y) "" X) . s implies ( x in X . s & x in Y . s ) )

assume
root-tree [x,s] in ((Reverse Y) "" X) . s
; :: thesis: ( x in X . s & x in Y . s )assume that

A3: x in X . s and

A4: x in Y . s ; :: thesis: root-tree [x,s] in ((Reverse Y) "" X) . s

A5: root-tree [x,s] in FreeGen (s,Y) by A4, MSAFREE:def 15;

[x,s] in the carrier of (DTConMSA Y) by A4, Th2;

then ((Reverse Y) . s) . (root-tree [x,s]) = [x,s] `1 by A1, A5, MSAFREE:def 17

.= x ;

then root-tree [x,s] in ((Reverse Y) . s) " (X . s) by A1, A2, A3, A5, FUNCT_1:def 7;

hence root-tree [x,s] in ((Reverse Y) "" X) . s by EQUATION:def 1; :: thesis: verum

end;A3: x in X . s and

A4: x in Y . s ; :: thesis: root-tree [x,s] in ((Reverse Y) "" X) . s

A5: root-tree [x,s] in FreeGen (s,Y) by A4, MSAFREE:def 15;

[x,s] in the carrier of (DTConMSA Y) by A4, Th2;

then ((Reverse Y) . s) . (root-tree [x,s]) = [x,s] `1 by A1, A5, MSAFREE:def 17

.= x ;

then root-tree [x,s] in ((Reverse Y) . s) " (X . s) by A1, A2, A3, A5, FUNCT_1:def 7;

hence root-tree [x,s] in ((Reverse Y) "" X) . s by EQUATION:def 1; :: thesis: verum

then A6: root-tree [x,s] in ((Reverse Y) . s) " (X . s) by EQUATION:def 1;

then A7: (Reverse (s,Y)) . (root-tree [x,s]) in X . s by A1, FUNCT_1:def 7;

A8: root-tree [x,s] in FreeGen (s,Y) by A1, A2, A6, FUNCT_1:def 7;

then consider z being set such that

A9: z in Y . s and

A10: root-tree [x,s] = root-tree [z,s] by MSAFREE:def 15;

B: [z,s] `1 = z ;

A11: [x,s] = [z,s] by A10, TREES_4:4;

then [x,s] in the carrier of (DTConMSA Y) by A9, Th2;

then [x,s] `1 in X . s by A8, A7, MSAFREE:def 17;

hence ( x in X . s & x in Y . s ) by A9, A11, B; :: thesis: verum