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) = dom (T with-replacement t,T1)

proof

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 ;
hence dom (tree T,{t},T1) = dom (T with-replacement t,T1) ; :: thesis: verum

end;

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 { (p' ^ s) where p' is Element of dom T, s is Element of dom T1 : p' 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 t' being Element of dom T such that
A6: ( q = t' & ( for p being FinSequence of NAT st p in {t} holds
not p is_a_prefix_of t' ) ) ;
consider p being FinSequence of NAT such that
A7: p = t ;
p in {t} by A7, TARSKI:def 1;
then A8: not p is_a_prefix_of t' by A6;
( 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 A7, Th16;
hence (tree T,{t},T1) . q = (T with-replacement t,T1) . q by A1, A2, A5, A6, A8, Th15; :: thesis: verum

end;

suppose A9: q in { (p' ^ s) where p' is Element of dom T, s is Element of dom T1 : p' 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
A10: ( q = p ^ r & p in {t} ) ;
A11: q in { (p ^ s) where s is Element of dom T1 : s = s } by A10;
consider p1 being Element of dom T, r1 being Element of dom T1 such that
A12: ( q = p1 ^ r1 & p1 in {t} & (tree T,{t},T1) . q = T1 . r1 ) by A2, A9, Th17;
A13: ( p1 = t & p = t ) by A10, A12, TARSKI:def 1;
then consider r2 being Element of dom T1 such that
A14: ( q = p ^ r2 & (T with-replacement p,T1) . q = T1 . r2 ) by A1, A2, A11, Th18;
thus (tree T,{t},T1) . q = (T with-replacement t,T1) . q by A12, A13, A14, 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