let D be non empty set ; 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; 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; ( 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)
; 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 ;
( 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
;
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;
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; verum