let D be non empty set ; :: thesis: for Z being DecoratedTree of D
for x1, x2 being Element of dom Z st x1 = <*0*> & x2 = <*1*> & succ (Root (dom Z)) = {x1,x2} holds
Z = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))
A1: not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:52;
set e = elementary_tree 2;
let Z be DecoratedTree of D; :: thesis: for x1, x2 being Element of dom Z st x1 = <*0*> & x2 = <*1*> & succ (Root (dom Z)) = {x1,x2} holds
Z = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))
let x1, x2 be Element of dom Z; :: thesis: ( x1 = <*0*> & x2 = <*1*> & succ (Root (dom Z)) = {x1,x2} implies Z = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)) )
assume that
A2: x1 = <*0*> and
A3: x2 = <*1*> and
A4: succ (Root (dom Z)) = {x1,x2} ; :: thesis: Z = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))
A5: dom (Z | x2) = (dom Z) | x2 by TREES_2:def 10;
set T1 = ((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1));
set E = (elementary_tree 2) --> (Root Z);
A6: dom (Z | x1) = (dom Z) | x1 by TREES_2:def 10;
set T = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2));
A7: <*0*> in elementary_tree 2 by ENUMSET1:def 1, TREES_1:53;
then A8: <*0*> in dom ((elementary_tree 2) --> (Root Z)) by FUNCOP_1:13;
then A9: dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) = (dom ((elementary_tree 2) --> (Root Z))) with-replacement (<*0*>,(dom (Z | x1))) by TREES_2:def 11;
<*1*> in elementary_tree 2 by ENUMSET1:def 1, TREES_1:53;
then <*1*> in dom ((elementary_tree 2) --> (Root Z)) by FUNCOP_1:13;
then A10: <*1*> in dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) by A8, A9, A1, TREES_1:def 9;
then A11: dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) = (dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1)))) with-replacement (<*1*>,(dom (Z | x2))) by TREES_2:def 11;
A12: dom ((elementary_tree 2) --> (Root Z)) = elementary_tree 2 by FUNCOP_1:13;
then A13: dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) = (elementary_tree 2) with-replacement (<*0*>,((dom Z) | x1)) by A7, A6, TREES_2:def 11;
A14: for s being FinSequence of NAT st s in dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) holds
((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s

proof

let s be FinSequence of NAT ; :: thesis: ( s in dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) implies ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s )
assume A15: s in dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) ; :: thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s
then A16: ( ( not <*1*> is_a_prefix_of s & ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) . s ) or ex u being FinSequence of NAT st
( u in dom (Z | x2) & s = <*1*> ^ u & ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = (Z | x2) . u ) ) by A10, A11, TREES_2:def 11;

now :: thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s

per cases ( ( s in dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in dom (Z | x2) & s = <*1*> ^ w ) ) by A10, A11, A15, TREES_1:def 9;

suppose A17: ( s in dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) & not <*1*> is_a_proper_prefix_of s ) ; :: thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s

then A18: ( ( not <*0*> is_a_prefix_of s & (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) . s = ((elementary_tree 2) --> (Root Z)) . s ) or ex u being FinSequence of NAT st
( u in dom (Z | x1) & s = <*0*> ^ u & (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) . s = (Z | x1) . u ) ) by A8, A9, TREES_2:def 11;

now :: thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s

per cases ( ( s in elementary_tree 2 & not <*0*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in (dom Z) | x1 & s = <*0*> ^ w ) ) by A7, A13, A17, TREES_1:def 9;

suppose A19: ( s in elementary_tree 2 & not <*0*> is_a_proper_prefix_of s ) ; :: thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s

now :: thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s

per cases ( s = {} or s = <*0*> or s = <*1*> ) by A19, ENUMSET1:def 1, TREES_1:53;

suppose A20: s = {} ; :: thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s

then ( ( for u being FinSequence of NAT holds
( not u in dom (Z | x2) or not s = <*1*> ^ u or not ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = (Z | x2) . u ) ) & ((elementary_tree 2) --> (Root Z)) . s = Z . s ) by A19, FUNCOP_1:7;
hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A10, A11, A15, A18, A20, TREES_2:def 11; :: thesis: verum

end;

suppose s = <*0*> ; :: thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s

hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A2, A3, A6, A5, A16, A18, TREES_2:def 10; :: thesis: verum

end;

suppose s = <*1*> ; :: thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s

hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A3, A5, A16, TREES_2:def 10; :: thesis: verum

end;

end;

end;

hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s ; :: thesis: verum

end;

suppose ex w being FinSequence of NAT st
( w in (dom Z) | x1 & s = <*0*> ^ w ) ; :: thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s

hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A2, A3, A6, A5, A16, A18, TREES_1:1, TREES_2:def 10; :: thesis: verum

end;

end;

end;

hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s ; :: thesis: verum

end;

suppose ex w being FinSequence of NAT st
( w in dom (Z | x2) & s = <*1*> ^ w ) ; :: thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s

hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A3, A5, A16, TREES_1:1, TREES_2:def 10; :: thesis: verum

end;

end;

end;

hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s ; :: thesis: verum

end;

dom Z = dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) by A2, A3, A4, A12, A6, A5, A9, A11, Th19;
hence Z = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)) by A14, TREES_2:31; :: thesis: verum