let T1, T2 be DecoratedTree; ( ex q being DTree-yielding FinSequence st
( p = q & dom T1 = tree (doms q) ) & T1 . {} = x & ( for n being Nat st n < len p holds
T1 | <*n*> = p . (n + 1) ) & ex q being DTree-yielding FinSequence st
( p = q & dom T2 = tree (doms q) ) & T2 . {} = x & ( for n being Nat st n < len p holds
T2 | <*n*> = p . (n + 1) ) implies T1 = T2 )
given q1 being DTree-yielding FinSequence such that A16:
p = q1
and
A17:
dom T1 = tree (doms q1)
; ( not T1 . {} = x or ex n being Nat st
( n < len p & not T1 | <*n*> = p . (n + 1) ) or for q being DTree-yielding FinSequence holds
( not p = q or not dom T2 = tree (doms q) ) or not T2 . {} = x or ex n being Nat st
( n < len p & not T2 | <*n*> = p . (n + 1) ) or T1 = T2 )
assume that
A18:
T1 . {} = x
and
A19:
for n being Nat st n < len p holds
T1 | <*n*> = p . (n + 1)
; ( for q being DTree-yielding FinSequence holds
( not p = q or not dom T2 = tree (doms q) ) or not T2 . {} = x or ex n being Nat st
( n < len p & not T2 | <*n*> = p . (n + 1) ) or T1 = T2 )
given q2 being DTree-yielding FinSequence such that A20:
( p = q2 & dom T2 = tree (doms q2) )
; ( not T2 . {} = x or ex n being Nat st
( n < len p & not T2 | <*n*> = p . (n + 1) ) or T1 = T2 )
assume that
A21:
T2 . {} = x
and
A22:
for n being Nat st n < len p holds
T2 | <*n*> = p . (n + 1)
; T1 = T2
now for q being FinSequence of NAT st q in dom T1 holds
T1 . q = T2 . qlet q be
FinSequence of
NAT ;
( q in dom T1 implies T1 . q = T2 . q )assume A23:
q in dom T1
;
T1 . q = T2 . qnow ( q <> {} implies T1 . q = T2 . q )assume
q <> {}
;
T1 . q = T2 . qthen consider s being
FinSequence of
NAT ,
n being
Element of
NAT such that A24:
q = <*n*> ^ s
by FINSEQ_2:130;
A25:
<*n*> in dom T1
by A23, A24, TREES_1:21;
A26:
n < len (doms q1)
by A17, A23, A24, TREES_3:48;
len (doms q1) = len p
by A16, TREES_3:38;
then A27:
(
T1 | <*n*> = p . (n + 1) &
T2 | <*n*> = p . (n + 1) )
by A19, A22, A26;
A28:
s in (dom T1) | <*n*>
by A23, A24, A25, TREES_1:def 6;
then
T1 . q = (T1 | <*n*>) . s
by A24, TREES_2:def 10;
hence
T1 . q = T2 . q
by A16, A17, A20, A24, A27, A28, TREES_2:def 10;
verum end; hence
T1 . q = T2 . q
by A18, A21;
verum end;
hence
T1 = T2
by A16, A17, A20; verum