let D be non empty set ; :: thesis: for Z being finite DecoratedTree of D
for z being Element of dom Z st succ (Root (dom Z)) = {z} holds
Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))
set e = elementary_tree 1;
let Z be finite DecoratedTree of D; :: thesis: for z being Element of dom Z st succ (Root (dom Z)) = {z} holds
Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))
let z be Element of dom Z; :: thesis: ( succ (Root (dom Z)) = {z} implies Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z)) )
set E = (elementary_tree 1) --> (Root Z);
A1: dom ((elementary_tree 1) --> (Root Z)) = elementary_tree 1 by FUNCOP_1:13;
A2: dom (Z | z) = (dom Z) | z by TREES_2:def 10;
A3: <*0*> in elementary_tree 1 by TARSKI:def 2, TREES_1:51;
then A4: <*0*> in dom ((elementary_tree 1) --> (Root Z)) by FUNCOP_1:13;
assume A5: succ (Root (dom Z)) = {z} ; :: thesis: Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))
then card (succ (Root (dom Z))) = 1 by CARD_1:30;
then branchdeg (Root (dom Z)) = 1 by TREES_2:def 12;
then {z} = {<*0*>} by A5, Th13;
then z in {<*0*>} by TARSKI:def 1;
then A6: z = <*0*> by TARSKI:def 1;
A7: for s being FinSequence of NAT st s in dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) holds
(((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s

proof

let s be FinSequence of NAT ; :: thesis: ( s in dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) implies (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s )
assume A8: s in dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) ; :: thesis: (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s
A9: dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) = (dom ((elementary_tree 1) --> (Root Z))) with-replacement (<*0*>,(dom (Z | z))) by A4, TREES_2:def 11;
then A10: ( ( not <*0*> is_a_prefix_of s & (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = ((elementary_tree 1) --> (Root Z)) . s ) or ex w being FinSequence of NAT st
( w in dom (Z | z) & s = <*0*> ^ w & (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = (Z | z) . w ) ) by A4, A8, TREES_2:def 11;

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

per cases ( ( s in dom ((elementary_tree 1) --> (Root Z)) & not <*0*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in dom (Z | z) & s = <*0*> ^ w ) ) by A4, A9, A8, TREES_1:def 9;

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

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

per cases ( s = {} or s = <*0*> ) by A11, TARSKI:def 2, TREES_1:51;

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

then s in elementary_tree 1 by TREES_1:22;
then A13: ((elementary_tree 1) --> (Root Z)) . s = Z . s by A12, FUNCOP_1:7;
for w being FinSequence of NAT holds
( not w in dom (Z | z) or not s = <*0*> ^ w or not (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = (Z | z) . w ) by A12;
hence (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s by A4, A9, A8, A13, TREES_2:def 11; :: thesis: verum

end;

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

hence (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s by A6, A2, A10, TREES_2:def 10; :: thesis: verum

end;

end;

end;

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

end;

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

hence (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s by A6, A2, A10, TREES_1:1, TREES_2:def 10; :: thesis: verum

end;

end;

end;

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

end;

dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) = (elementary_tree 1) with-replacement (<*0*>,((dom Z) | z)) by A3, A1, A2, TREES_2:def 11;
then dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) = dom Z by A5, Th17;
hence Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z)) by A7, TREES_2:31; :: thesis: verum