let x be object ; :: 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 FINSEQ_3:132
.= ^ (dom T) by TREES_3:def 16
.= (elementary_tree 1) with-replacement (<*0*>,(dom T)) by TREES_3:58 ;
A2: dom ((elementary_tree 1) --> x) = elementary_tree 1 ;
reconsider t1 = {} , t2 = <*0*> as Element of elementary_tree 1 by TARSKI:def 2, TREES_1:51;
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 11;
A4: {} in dom T by TREES_1:22;
now :: thesis: for y being object st y in (elementary_tree 1) with-replacement (<*0*>,(dom T)) holds
(((elementary_tree 1) --> x) with-replacement (<*0*>,T)) . y = (x -tree <*T*>) . y
let y be object ; :: 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 9;
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:34, TARSKI:def 2, TREES_1:51;
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:45
.= x
.= (x -tree <*T*>) . {} by Def4 ;
now :: thesis: ( ex r being FinSequence of NAT st
( r in dom T & q = <*0*> ^ r ) implies (((elementary_tree 1) --> x) with-replacement (<*0*>,T)) . q = (x -tree <*T*>) . q )
given r being FinSequence of NAT such that A7: r in dom T and
A8: 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 A8;
then A9: (((elementary_tree 1) --> x) with-replacement (<*0*>,T)) . q = T . r by A2, TREES_3:46;
( 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 (<*0*>,(dom T))) | t2 = dom T by TREES_1:33;
hence (((elementary_tree 1) --> x) with-replacement (<*0*>,T)) . q = (x -tree <*T*>) . q by A1, A8, A9, A10, TREES_2:def 10; :: 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; :: thesis: verum