let T, T1 be DecoratedTree; :: thesis: for t being Element of dom T holds tree (T,{t},T1) = T with-replacement (t,T1)
let t be Element of dom T; :: thesis: tree (T,{t},T1) = T with-replacement (t,T1)
A1: dom (tree (T,{t},T1)) = tree ((dom T),{t},(dom T1)) by Def2
.= (dom T) with-replacement (t,(dom T1)) by Th10
.= dom (T with-replacement (t,T1)) by TREES_2:def 12 ;
for q being FinSequence of NAT st q in dom (tree (T,{t},T1)) holds
(tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q

proof

let q be FinSequence of NAT ; :: thesis: ( q in dom (tree (T,{t},T1)) implies (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q )
assume A3: q in dom (tree (T,{t},T1)) ; :: thesis: (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q
then A4: q in tree ((dom T),{t},(dom T1)) by Def2;
A5: tree ((dom T),{t},(dom T1)) = { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in {t} holds
not p is_a_prefix_of t1 } \/ { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in {t} } by Th7;

per cases ( q in { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in {t} holds
not p is_a_prefix_of t1 } or q in { (p9 ^ s) where p9 is Element of dom T, s is Element of dom T1 : p9 in {t} } ) by A4, A5, XBOOLE_0:def 3;

suppose A6: q in { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in {t} holds
not p is_a_prefix_of t1 } ; :: thesis: (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q

then consider t9 being Element of dom T such that
A7: q = t9 and
A8: for p being FinSequence of NAT st p in {t} holds
not p is_a_prefix_of t9 ;
consider p being FinSequence of NAT such that
A9: p = t ;
p in {t} by A9, TARSKI:def 1;
then A11: not p is_a_prefix_of t9 by A8;
( q in dom (T with-replacement (t,T1)) & q in { t1 where t1 is Element of dom T : not p is_a_prefix_of t1 } implies (T with-replacement (t,T1)) . q = T . q ) by A9, Th16;
hence (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q by A1, A3, A6, A7, A11, Th15; :: thesis: verum

end;

suppose A13: q in { (p9 ^ s) where p9 is Element of dom T, s is Element of dom T1 : p9 in {t} } ; :: thesis: (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q

then consider p being Element of dom T, r being Element of dom T1 such that
A14: q = p ^ r and
A15: p in {t} ;
A16: q in { (p ^ s) where s is Element of dom T1 : s = s } by A14;
consider p1 being Element of dom T, r1 being Element of dom T1 such that
A17: q = p1 ^ r1 and
A18: p1 in {t} and
A19: (tree (T,{t},T1)) . q = T1 . r1 by A3, A13, Th17;
A20: p1 = t by A18, TARSKI:def 1;
A21: p = t by A15, TARSKI:def 1;
then ex r2 being Element of dom T1 st
( q = p ^ r2 & (T with-replacement (p,T1)) . q = T1 . r2 ) by A1, A3, A16, Th18;
hence (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q by A17, A19, A20, A21, FINSEQ_1:46; :: thesis: verum

end;

end;

end;

hence tree (T,{t},T1) = T with-replacement (t,T1) by A1, TREES_2:33; :: thesis: verum