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 Th9
.= dom (T with-replacement (t,T1)) by TREES_2:def 11 ;
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 A2: q in dom (tree (T,{t},T1)) ; :: thesis: (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q
then A3: q in tree ((dom T),{t},(dom T1)) by Def2;
A4: 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 A3, A4, XBOOLE_0:def 3;

suppose A5: 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
A6: q = t9 and
A7: 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
A8: p = t ;
p in {t} by A8, TARSKI:def 1;
then A9: not p is_a_prefix_of t9 by A7;
( 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 A8, Th13;
hence (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q by A1, A2, A5, A6, A9, Th12; :: thesis: verum

end;

suppose A10: 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
A11: q = p ^ r and
A12: p in {t} ;
A13: q in { (p ^ s) where s is Element of dom T1 : verum } by A11;
consider p1 being Element of dom T, r1 being Element of dom T1 such that
A14: q = p1 ^ r1 and
A15: p1 in {t} and
A16: (tree (T,{t},T1)) . q = T1 . r1 by A2, A10, Th14;
A17: p1 = t by A15, TARSKI:def 1;
A18: p = t by A12, 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, A2, A13, Th15;
hence (tree (T,{t},T1)) . q = (T with-replacement (t,T1)) . q by A14, A16, A17, A18, FINSEQ_1:33; :: thesis: verum

end;

end;

end;

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