let D be non empty set ; :: thesis: for Z being DecoratedTree of
for x1, x2 being Element of dom Z st dom Z is finite & 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 Z be DecoratedTree of ; :: thesis: for x1, x2 being Element of dom Z st dom Z is finite & 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: ( dom Z is finite & 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 A1: ( dom Z is finite & x1 = <*0 *> & x2 = <*1*> & succ (Root (dom Z)) = {x1,x2} ) ; :: thesis: Z = (((elementary_tree 2) --> (Root Z)) with-replacement <*0 *>,(Z | x1)) with-replacement <*1*>,(Z | x2)
set e = elementary_tree 2;
set E = (elementary_tree 2) --> (Root Z);
A2: ( <*0 *> in elementary_tree 2 & <*1*> in elementary_tree 2 ) by ENUMSET1:def 1, TREES_1:90;
A3: dom ((elementary_tree 2) --> (Root Z)) = elementary_tree 2 by FUNCOP_1:19;
A4: ( <*0 *> in dom ((elementary_tree 2) --> (Root Z)) & <*1*> in dom ((elementary_tree 2) --> (Root Z)) ) by A2, FUNCOP_1:19;
A5: ( dom (Z | x1) = (dom Z) | x1 & dom (Z | x2) = (dom Z) | x2 ) by TREES_2:def 11;
set T1 = ((elementary_tree 2) --> (Root Z)) with-replacement <*0 *>,(Z | x1);
set T = (((elementary_tree 2) --> (Root Z)) with-replacement <*0 *>,(Z | x1)) with-replacement <*1*>,(Z | x2);
A6: dom (((elementary_tree 2) --> (Root Z)) with-replacement <*0 *>,(Z | x1)) = (dom ((elementary_tree 2) --> (Root Z))) with-replacement <*0 *>,(dom (Z | x1)) by A4, TREES_2:def 12;
A7: dom (((elementary_tree 2) --> (Root Z)) with-replacement <*0 *>,(Z | x1)) = (elementary_tree 2) with-replacement <*0 *>,((dom Z) | x1) by A2, A3, A5, TREES_2:def 12;
not <*0 *> is_a_proper_prefix_of <*1*> by TREES_1:89;
then A8: <*1*> in dom (((elementary_tree 2) --> (Root Z)) with-replacement <*0 *>,(Z | x1)) by A4, A6, TREES_1:def 12;
then A9: 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;
then A10: dom Z = dom ((((elementary_tree 2) --> (Root Z)) with-replacement <*0 *>,(Z | x1)) with-replacement <*1*>,(Z | x2)) by A1, A3, A5, A6, Th29;
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 A11: 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 A12: ( ( 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 A8, A9, 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 A8, A9, A11, TREES_1:def 12;

suppose A13: ( 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 A14: ( ( 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 A4, A6, 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 A2, A7, A13, TREES_1:def 12;

suppose A15: ( 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 A15, ENUMSET1:def 1, TREES_1:90;

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

then A17: 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 A15, A16, FUNCOP_1:13;
hence ((((elementary_tree 2) --> (Root Z)) with-replacement <*0 *>,(Z | x1)) with-replacement <*1*>,(Z | x2)) . s = Z . s by A8, A9, A11, A14, A16, A17, 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 A1, A5, A12, A14, 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 A1, A5, A12, 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 A1, A5, A12, A14, 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 A1, A5, A12, 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;

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