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;

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

hence
x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,T)
by A1, A3; :: thesis: verum(((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 ;

end;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 )

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