let x be set ; 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; 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; 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; 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; ( ( 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 ( root-tree [x,s] in ((Reverse Y) "" X) . s implies ( x in X . s & x in Y . s ) )
assume that A3:
x in X . s
and A4:
x in Y . s
;
root-tree [x,s] in ((Reverse Y) "" X) . sA5:
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;
verum
end;
assume
root-tree [x,s] in ((Reverse Y) "" X) . s
; ( x in X . s & x in Y . s )
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; verum