let D be non empty set ; :: thesis: for Z, Z1, Z2 being DecoratedTree of
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 ; :: 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 T1 = Z with-replacement z,Z1;
set T2 = Z with-replacement z,Z2;
A2: dom (Z with-replacement z,Z1) = (dom Z) with-replacement z,(dom Z1) by TREES_2:def 12;
A3: dom (Z with-replacement z,Z2) = (dom Z) with-replacement z,(dom Z2) by TREES_2:def 12;
A4: (dom Z) with-replacement z,(dom Z1) = (dom Z) with-replacement z,(dom Z2) by A1, A2, TREES_2:def 12;
A5: dom Z1 = dom Z2 by A1, A2, A3, Th15;
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 )
assume s in dom Z1 ; :: thesis: Z1 . s = Z2 . s
then A6: ( z ^ s in (dom Z) with-replacement z,(dom Z2) & z ^ s in (dom Z) with-replacement z,(dom Z1) ) by A4, TREES_1:def 12;
A7: z is_a_prefix_of z ^ s by TREES_1:8;
then consider w being FinSequence of NAT such that
A8: ( w in dom Z2 & z ^ s = z ^ w & (Z with-replacement z,Z2) . (z ^ s) = Z2 . w ) by A6, TREES_2:def 12;
A9: 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 A6, A7, TREES_2:def 12;
s = w by A8, FINSEQ_1:46;
hence Z1 . s = Z2 . s by A1, A8, A9, FINSEQ_1:46; :: thesis: verum

end;

hence Z1 = Z2 by A5, TREES_2:33; :: thesis: verum