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:19;
A2: dom (Z | z) = (dom Z) | z by TREES_2:def 11;
A3: <*0 *> in elementary_tree 1 by TARSKI:def 2, TREES_1:88;
then A4: <*0 *> in dom ((elementary_tree 1) --> (Root Z)) by FUNCOP_1:19;
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:50;
then branchdeg (Root (dom Z)) = 1 by TREES_2:def 13;
then {z} = {<*0 *>} by A5, Th23;
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 12;
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 12;

now

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

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

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

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:47;
then A13: ((elementary_tree 1) --> (Root Z)) . s = Z . s by A12, FUNCOP_1:13;
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 12; :: 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 11; :: 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:8, TREES_2:def 11; :: 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 12;
then dom (((elementary_tree 1) --> (Root Z)) with-replacement <*0 *>,(Z | z)) = dom Z by A5, Th27;
hence Z = ((elementary_tree 1) --> (Root Z)) with-replacement <*0 *>,(Z | z) by A7, TREES_2:33; :: thesis: verum