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

A31: now

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

A33: now

assume A34: q <> {} ; :: thesis: T1 . q = T2 . q
consider s being FinSequence of NAT , n being Nat such that
A35: q = <*n*> ^ s by A34, 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;
A38: len (doms q1) = len p by A24, TREES_3:40;
A39: ( T1 | <*n*> = p . (n + 1) & T2 | <*n*> = p . (n + 1) ) by A27, A30, A37, A38;
A40: s in (dom T1) | <*n*> by A32, A35, A36, TREES_1:def 9;
A41: T1 . q = (T1 | <*n*>) . s by A35, A40, TREES_2:def 11;
thus T1 . q = T2 . q by A24, A25, A28, A35, A39, A40, A41, TREES_2:def 11; :: thesis: verum

end;

thus T1 . q = T2 . q by A26, A29, A33; :: thesis: verum

end;

thus T1 = T2 by A24, A25, A28, A31, TREES_2:33; :: thesis: verum