let T1, T2 be DecoratedTree; :: thesis: ( 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) ; :: thesis: ( 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) ; :: thesis: ( 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) ) ; :: thesis: ( 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) ; :: thesis: T1 = T2

( 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) ; :: thesis: ( 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) ; :: thesis: ( 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) ) ; :: thesis: ( 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) ; :: thesis: T1 = T2

now :: thesis: for q being FinSequence of NAT st q in dom T1 holds

T1 . q = T2 . q

hence
T1 = T2
by A16, A17, A20; :: thesis: verumT1 . q = T2 . q

let q be FinSequence of NAT ; :: thesis: ( q in dom T1 implies T1 . q = T2 . q )

assume A23: q in dom T1 ; :: thesis: T1 . q = T2 . q

end;assume A23: q in dom T1 ; :: thesis: T1 . q = T2 . q

now :: thesis: ( q <> {} implies T1 . q = T2 . q )

hence
T1 . q = T2 . q
by A18, A21; :: thesis: verumassume
q <> {}
; :: thesis: T1 . q = T2 . q

then 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; :: thesis: verum

end;then 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; :: thesis: verum