let D1, D2 be non empty set ; for d1 being Element of D1
for d2 being Element of D2
for F being non empty DTree-set of D1,D2
for F2 being non empty DTree-set of D2
for p being FinSequence of F
for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Nat st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) holds
([d1,d2] -tree p) `2 = d2 -tree p2
let d1 be Element of D1; for d2 being Element of D2
for F being non empty DTree-set of D1,D2
for F2 being non empty DTree-set of D2
for p being FinSequence of F
for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Nat st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) holds
([d1,d2] -tree p) `2 = d2 -tree p2
let d2 be Element of D2; for F being non empty DTree-set of D1,D2
for F2 being non empty DTree-set of D2
for p being FinSequence of F
for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Nat st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) holds
([d1,d2] -tree p) `2 = d2 -tree p2
let F be non empty DTree-set of D1,D2; for F2 being non empty DTree-set of D2
for p being FinSequence of F
for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Nat st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) holds
([d1,d2] -tree p) `2 = d2 -tree p2
let F2 be non empty DTree-set of D2; for p being FinSequence of F
for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Nat st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) holds
([d1,d2] -tree p) `2 = d2 -tree p2
let p be FinSequence of F; for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Nat st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) holds
([d1,d2] -tree p) `2 = d2 -tree p2
let p2 be FinSequence of F2; ( dom p2 = dom p & ( for i being Nat st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) implies ([d1,d2] -tree p) `2 = d2 -tree p2 )
assume that
A1:
dom p2 = dom p
and
A2:
for i being Nat st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2
; ([d1,d2] -tree p) `2 = d2 -tree p2
set W = [d1,d2] -tree p;
set W2 = d2 -tree p2;
A3:
len (doms p) = len p
by TREES_3:38;
A4:
len (doms p2) = len p2
by TREES_3:38;
A5:
len p = len p2
by A1, FINSEQ_3:29;
then A6:
dom (doms p) = dom (doms p2)
by A3, A4, FINSEQ_3:29;
A7:
dom (doms p) = dom p
by A3, FINSEQ_3:29;
then A11:
doms p = doms p2
by A6, A7, FINSEQ_1:13;
dom (([d1,d2] -tree p) `2) =
dom ([d1,d2] -tree p)
by Th24
.=
tree (doms p)
by Th10
;
hence
dom (([d1,d2] -tree p) `2) = dom (d2 -tree p2)
by A11, Th10; TREES_4:def 1 for p being Node of (([d1,d2] -tree p) `2) holds (([d1,d2] -tree p) `2) . p = (d2 -tree p2) . p
let x be Node of (([d1,d2] -tree p) `2); (([d1,d2] -tree p) `2) . x = (d2 -tree p2) . x
reconsider a = x as Node of ([d1,d2] -tree p) by Th24;
A12:
(([d1,d2] -tree p) `2) . x = (([d1,d2] -tree p) . a) `2
by TREES_3:39;
per cases
( x = {} or x <> {} )
;
suppose
x <> {}
;
(([d1,d2] -tree p) `2) . x = (d2 -tree p2) . xthen consider n being
Nat,
T being
DecoratedTree,
q being
Node of
T such that A13:
n < len p
and A14:
T = p . (n + 1)
and A15:
a = <*n*> ^ q
by Th11;
reconsider T =
T as
Element of
F by A13, A14, Lm3;
reconsider q =
q as
Node of
(T `2) by Th24;
A16:
p2 . (n + 1) = T `2
by A2, A13, A14, Lm2;
A17:
([d1,d2] -tree p) . a = T . q
by A13, A14, A15, Th12;
(d2 -tree p2) . a = (T `2) . q
by A5, A13, A15, A16, Th12;
hence
(([d1,d2] -tree p) `2) . x = (d2 -tree p2) . x
by A12, A17, TREES_3:39;
verum end; end;