let x be set ; :: thesis: for T being DecoratedTree holds x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement <*0 *>,T
let T be DecoratedTree; :: thesis: x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement <*0 *>,T
set D = ((elementary_tree 1) --> x) with-replacement <*0 *>,T;
set W = (elementary_tree 1) with-replacement <*0 *>,(dom T);
A1: dom (x -tree <*T*>) = tree (doms <*T*>) by Th10
.= tree <*(dom T)*> by FUNCT_6:33
.= ^ (dom T) by TREES_3:def 16
.= (elementary_tree 1) with-replacement <*0 *>,(dom T) by TREES_3:61 ;
A2: dom ((elementary_tree 1) --> x) = elementary_tree 1 by FUNCOP_1:19;
reconsider t1 = {} , t2 = <*0 *> as Element of elementary_tree 1 by TARSKI:def 2, TREES_1:88;
t2 = t2 ;
then A4: dom (((elementary_tree 1) --> x) with-replacement <*0 *>,T) = (elementary_tree 1) with-replacement <*0 *>,(dom T) by A2, TREES_2:def 12;
A5: {} in dom T by TREES_1:47;

now

let y be set ; :: thesis: ( y in (elementary_tree 1) with-replacement <*0 *>,(dom T) implies (((elementary_tree 1) --> x) with-replacement <*0 *>,T) . y = (x -tree <*T*>) . y )
assume y in (elementary_tree 1) with-replacement <*0 *>,(dom T) ; :: thesis: (((elementary_tree 1) --> x) with-replacement <*0 *>,T) . y = (x -tree <*T*>) . y
then reconsider q = y as Element of (elementary_tree 1) with-replacement <*0 *>,(dom T) ;
( q in elementary_tree 1 or ex v being FinSequence of NAT st
( v in dom T & q = t2 ^ v ) ) by TREES_1:def 12;
then A9: ( q = {} or ( q = t2 & t2 = t2 ^ t1 ) or ex v being FinSequence of NAT st
( v in dom T & q = <*0 *> ^ v ) ) by FINSEQ_1:47, TARSKI:def 2, TREES_1:88;
not t2 is_a_prefix_of t1 ;
then A11: (((elementary_tree 1) --> x) with-replacement <*0 *>,T) . {} = ((elementary_tree 1) --> x) . t1 by A2, TREES_3:48
.= x by FUNCOP_1:13
.= (x -tree <*T*>) . {} by Def4 ;

now

given r being FinSequence of NAT such that A13: r in dom T and
A14: q = <*0 *> ^ r ; :: thesis: (((elementary_tree 1) --> x) with-replacement <*0 *>,T) . q = (x -tree <*T*>) . q
reconsider r = r as Node of T by A13;
q = t2 ^ r by A14;
then A16: (((elementary_tree 1) --> x) with-replacement <*0 *>,T) . q = T . r by A2, TREES_3:49;
( len <*T*> = 1 & <*T*> . (0 + 1) = T ) by FINSEQ_1:57;
then A18: (x -tree <*T*>) | t2 = T by Def4;
((elementary_tree 1) with-replacement <*0 *>,(dom T)) | t2 = dom T by TREES_1:66;
hence (((elementary_tree 1) --> x) with-replacement <*0 *>,T) . q = (x -tree <*T*>) . q by A1, A14, A16, A18, TREES_2:def 11; :: thesis: verum

end;

hence (((elementary_tree 1) --> x) with-replacement <*0 *>,T) . y = (x -tree <*T*>) . y by A5, A9, A11; :: thesis: verum

end;

hence x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement <*0 *>,T by A1, A4, FUNCT_1:9; :: thesis: verum