let D be non empty set ; :: thesis: for Z, Z1, Z2 being DecoratedTree of D
for z being Element of dom Z st Z with-replacement z,Z1 = Z with-replacement z,Z2 holds
Z1 = Z2
let Z, Z1, Z2 be DecoratedTree of D; :: thesis: for z being Element of dom Z st Z with-replacement z,Z1 = Z with-replacement z,Z2 holds
Z1 = Z2
let z be Element of dom Z; :: thesis: ( Z with-replacement z,Z1 = Z with-replacement z,Z2 implies Z1 = Z2 )
assume A1: Z with-replacement z,Z1 = Z with-replacement z,Z2 ; :: thesis: Z1 = Z2
set T2 = Z with-replacement z,Z2;
set T1 = Z with-replacement z,Z1;
A2: dom (Z with-replacement z,Z1) = (dom Z) with-replacement z,(dom Z1) by TREES_2:def 12;
then A3: (dom Z) with-replacement z,(dom Z1) = (dom Z) with-replacement z,(dom Z2) by A1, TREES_2:def 12;
A4: for s being FinSequence of NAT st s in dom Z1 holds
Z1 . s = Z2 . s

proof

let s be FinSequence of NAT ; :: thesis: ( s in dom Z1 implies Z1 . s = Z2 . s )
A5: z is_a_prefix_of z ^ s by TREES_1:8;
assume A6: s in dom Z1 ; :: thesis: Z1 . s = Z2 . s
then z ^ s in (dom Z) with-replacement z,(dom Z1) by TREES_1:def 12;
then A7: ex u being FinSequence of NAT st
( u in dom Z1 & z ^ s = z ^ u & (Z with-replacement z,Z1) . (z ^ s) = Z1 . u ) by A5, TREES_2:def 12;
z ^ s in (dom Z) with-replacement z,(dom Z2) by A3, A6, TREES_1:def 12;
then consider w being FinSequence of NAT such that
w in dom Z2 and
A8: z ^ s = z ^ w and
A9: (Z with-replacement z,Z2) . (z ^ s) = Z2 . w by A5, TREES_2:def 12;
s = w by A8, FINSEQ_1:46;
hence Z1 . s = Z2 . s by A1, A9, A7, FINSEQ_1:46; :: thesis: verum

end;

dom (Z with-replacement z,Z2) = (dom Z) with-replacement z,(dom Z2) by TREES_2:def 12;
hence Z1 = Z2 by A1, A2, A4, Th15, TREES_2:33; :: thesis: verum