let D be non empty set ; :: thesis: for Z being finite DecoratedTree of
for z being Element of dom Z st succ (Root (dom Z)) = {z} & dom Z is finite holds
Z = ((elementary_tree 1) --> (Root Z)) with-replacement <*0 *>,(Z | z)
let Z be finite DecoratedTree of ; :: thesis: for z being Element of dom Z st succ (Root (dom Z)) = {z} & dom Z is finite 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} & dom Z is finite implies Z = ((elementary_tree 1) --> (Root Z)) with-replacement <*0 *>,(Z | z) )
assume A1: ( succ (Root (dom Z)) = {z} & dom Z is finite ) ; :: 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 A1, Th23;
then z in {<*0 *>} by TARSKI:def 1;
then A2: z = <*0 *> by TARSKI:def 1;
set e = elementary_tree 1;
set E = (elementary_tree 1) --> (Root Z);
A3: <*0 *> in elementary_tree 1 by TARSKI:def 2, TREES_1:88;
A4: ( dom ((elementary_tree 1) --> (Root Z)) = elementary_tree 1 & rng ((elementary_tree 1) --> (Root Z)) = {(Root Z)} ) by FUNCOP_1:14, FUNCOP_1:19;
A5: <*0 *> in dom ((elementary_tree 1) --> (Root Z)) by A3, FUNCOP_1:19;
A6: dom (Z | z) = (dom Z) | z by TREES_2:def 11;
then dom (((elementary_tree 1) --> (Root Z)) with-replacement <*0 *>,(Z | z)) = (elementary_tree 1) with-replacement <*0 *>,((dom Z) | z) by A3, A4, TREES_2:def 12;
then A7: dom (((elementary_tree 1) --> (Root Z)) with-replacement <*0 *>,(Z | z)) = dom Z by A1, Th27;
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

A8: dom (((elementary_tree 1) --> (Root Z)) with-replacement <*0 *>,(Z | z)) = (dom ((elementary_tree 1) --> (Root Z))) with-replacement <*0 *>,(dom (Z | z)) by A5, TREES_2:def 12;
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 A9: 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
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 A5, 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 A5, A8, A9, 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 A4, 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 A13: s in elementary_tree 1 by TREES_1:47;
A14: 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;
((elementary_tree 1) --> (Root Z)) . s = Z . s by A12, A13, FUNCOP_1:13;
hence (((elementary_tree 1) --> (Root Z)) with-replacement <*0 *>,(Z | z)) . s = Z . s by A5, A8, A9, A14, 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 A2, A6, 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 A2, A6, 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;

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