let x be object ; :: thesis: for T being DecoratedTree holds x -tree <*T*> = (() --> x) with-replacement (,T)
let T be DecoratedTree; :: thesis: x -tree <*T*> = (() --> x) with-replacement (,T)
set D = (() --> x) with-replacement (,T);
set W = () with-replacement (,(dom T));
A1: dom () = tree () by Th10
.= tree <*(dom T)*> by FINSEQ_3:132
.= ^ (dom T) by TREES_3:def 16
.= () with-replacement (,(dom T)) by TREES_3:58 ;
A2: dom (() --> x) = elementary_tree 1 ;
reconsider t1 = {} , t2 = as Element of elementary_tree 1 by ;
t2 = t2 ;
then A3: dom ((() --> x) with-replacement (,T)) = () with-replacement (,(dom T)) by ;
A4: {} in dom T by TREES_1:22;
now :: thesis: for y being object st y in () with-replacement (,(dom T)) holds
((() --> x) with-replacement (,T)) . y = () . y
let y be object ; :: thesis: ( y in () with-replacement (,(dom T)) implies ((() --> x) with-replacement (,T)) . y = () . y )
assume y in () with-replacement (,(dom T)) ; :: thesis: ((() --> x) with-replacement (,T)) . y = () . y
then reconsider q = y as Element of () with-replacement (,(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 9;
then A5: ( q = {} or ( q = t2 & t2 = t2 ^ t1 ) or ex v being FinSequence of NAT st
( v in dom T & q = ^ v ) ) by ;
not t2 is_a_prefix_of t1 ;
then A6: ((() --> x) with-replacement (,T)) . {} = (() --> x) . t1 by
.= x
.= () . {} by Def4 ;
now :: thesis: ( ex r being FinSequence of NAT st
( r in dom T & q = ^ r ) implies ((() --> x) with-replacement (,T)) . q = () . q )
given r being FinSequence of NAT such that A7: r in dom T and
A8: q = ^ r ; :: thesis: ((() --> x) with-replacement (,T)) . q = () . q
reconsider r = r as Node of T by A7;
q = t2 ^ r by A8;
then A9: (((elementary_tree 1) --> x) with-replacement (,T)) . q = T . r by ;
( len <*T*> = 1 & <*T*> . (0 + 1) = T ) by FINSEQ_1:40;
then A10: (x -tree <*T*>) | t2 = T by Def4;
((elementary_tree 1) with-replacement (,(dom T))) | t2 = dom T by TREES_1:33;
hence (((elementary_tree 1) --> x) with-replacement (,T)) . q = () . q by ; :: thesis: verum
end;
hence (((elementary_tree 1) --> x) with-replacement (,T)) . y = () . y by A4, A5, A6; :: thesis: verum
end;
hence x -tree <*T*> = (() --> x) with-replacement (,T) by A1, A3; :: thesis: verum