let D be non empty set ; 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; 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; ( 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}
; 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 ;
( 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)))
;
(((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;
hence
(((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s
;
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; verum