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:89;
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 11;
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 11;
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:90;
then A8: <*0 *> in dom ((elementary_tree 2) --> (Root Z)) by FUNCOP_1:19;
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 12;
<*1*> in elementary_tree 2 by ENUMSET1:def 1, TREES_1:90;
then <*1*> in dom ((elementary_tree 2) --> (Root Z)) by FUNCOP_1:19;
then A10: <*1*> in dom (((elementary_tree 2) --> (Root Z)) with-replacement <*0 *>,(Z | x1)) by A8, A9, A1, TREES_1:def 12;
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 12;
A12: dom ((elementary_tree 2) --> (Root Z)) = elementary_tree 2 by FUNCOP_1:19;
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 12;
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 12;

now

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 12;

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 12;

now

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 12;

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

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

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:13;
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 12; :: 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 11; :: 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 11; :: 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:8, TREES_2:def 11; :: 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:8, TREES_2:def 11; :: 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, Th29;
hence Z = (((elementary_tree 2) --> (Root Z)) with-replacement <*0 *>,(Z | x1)) with-replacement <*1*>,(Z | x2) by A14, TREES_2:33; :: thesis: verum