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 A3: dom (((elementary_tree 1) --> x) with-replacement <*0 *>,T) = (elementary_tree 1) with-replacement <*0 *>,(dom T) by A2, TREES_2:def 12;
A4: ( {} in dom T & <*0 *> ^ {} = <*0 *> & not <*0 *> is_a_proper_prefix_of {} & {} NAT = {} ) by FINSEQ_1:47, TREES_1:47, XBOOLE_1:115;

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 A5: ( 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 A6: (((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 A7: ( r in dom T & 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 A7;
q = t2 ^ r by A7;
then A8: (((elementary_tree 1) --> x) with-replacement <*0 *>,T) . q = T . r by A2, TREES_3:49;
( len <*T*> = 1 & <*T*> . (0 + 1) = T & 0 < 1 ) by FINSEQ_1:57;
then ( (x -tree <*T*>) | t2 = T & ((elementary_tree 1) with-replacement <*0 *>,(dom T)) | t2 = dom T ) by Def4, TREES_1:66;
hence (((elementary_tree 1) --> x) with-replacement <*0 *>,T) . q = (x -tree <*T*>) . q by A1, A7, A8, TREES_2:def 11; :: thesis: verum

end;

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

end;

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