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 11;
then A3: (dom Z) with-replacement (z,(dom Z1)) = (dom Z) with-replacement (z,(dom Z2)) by A1, TREES_2:def 11;
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:1;
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 9;
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 11;
z ^ s in (dom Z) with-replacement (z,(dom Z2)) by A3, A6, TREES_1:def 9;
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 11;
s = w by A8, FINSEQ_1:33;
hence Z1 . s = Z2 . s by A1, A9, A7, FINSEQ_1:33; :: thesis: verum

end;

dom (Z with-replacement (z,Z2)) = (dom Z) with-replacement (z,(dom Z2)) by TREES_2:def 11;
hence Z1 = Z2 by A1, A2, A4, Th6, TREES_2:31; :: thesis: verum