let T1, T2 be DecoratedTree; ( ex q being DTree-yielding FinSequence st
( p = q & dom T1 = tree (doms q) ) & T1 . {} = x & ( for n being Element of 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 Element of NAT st n < len p holds
T2 | <*n*> = p . (n + 1) ) implies T1 = T2 )
given q1 being DTree-yielding FinSequence such that A24:
p = q1
and
A25:
dom T1 = tree (doms q1)
; ( not T1 . {} = x or ex n being Element of 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 Element of NAT st
( n < len p & not T2 | <*n*> = p . (n + 1) ) or T1 = T2 )
assume that
A26:
T1 . {} = x
and
A27:
for n being Element of 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 Element of NAT st
( n < len p & not T2 | <*n*> = p . (n + 1) ) or T1 = T2 )
given q2 being DTree-yielding FinSequence such that A28:
( p = q2 & dom T2 = tree (doms q2) )
; ( not T2 . {} = x or ex n being Element of NAT st
( n < len p & not T2 | <*n*> = p . (n + 1) ) or T1 = T2 )
assume that
A29:
T2 . {} = x
and
A30:
for n being Element of NAT st n < len p holds
T2 | <*n*> = p . (n + 1)
; T1 = T2
now let q be
FinSequence of
NAT ;
( q in dom T1 implies T1 . q = T2 . q )assume A32:
q in dom T1
;
T1 . q = T2 . qnow assume
q <> {}
;
T1 . q = T2 . qthen consider s being
FinSequence of
NAT ,
n being
Nat such that A35:
q = <*n*> ^ s
by FINSEQ_2:150;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
A36:
<*n*> in dom T1
by A32, A35, TREES_1:46;
A37:
n < len (doms q1)
by A25, A32, A35, TREES_3:51;
len (doms q1) = len p
by A24, TREES_3:40;
then A39:
(
T1 | <*n*> = p . (n + 1) &
T2 | <*n*> = p . (n + 1) )
by A27, A30, A37;
A40:
s in (dom T1) | <*n*>
by A32, A35, A36, TREES_1:def 9;
then
T1 . q = (T1 | <*n*>) . s
by A35, TREES_2:def 11;
hence
T1 . q = T2 . q
by A24, A25, A28, A35, A39, A40, TREES_2:def 11;
verum end; hence
T1 . q = T2 . q
by A26, A29;
verum end;
hence
T1 = T2
by A24, A25, A28, TREES_2:33; verum