let Z be finite Tree; for z being Element of Z st succ (Root Z) = {z} holds
Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z))
let z be Element of Z; ( succ (Root Z) = {z} implies Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z)) )
set e = elementary_tree 1;
A1:
<*0*> in elementary_tree 1
by TARSKI:def 2, TREES_1:51;
A2:
{} in Z
by TREES_1:22;
assume A3:
succ (Root Z) = {z}
; Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z))
then
card (succ (Root Z)) = 1
by CARD_1:30;
then
branchdeg (Root Z) = 1
by TREES_2:def 12;
then
{z} = {<*0*>}
by A3, Th13;
then
z in {<*0*>}
by TARSKI:def 1;
then A4:
z = <*0*>
by TARSKI:def 1;
then A5:
<*0*> in Z
;
now for x being object holds
( ( x in Z implies x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ) & ( x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) implies x in Z ) )let x be
object ;
( ( x in Z implies x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ) & ( x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) implies b1 in Z ) )thus
(
x in Z implies
x in (elementary_tree 1) with-replacement (
<*0*>,
(Z | z)) )
( x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) implies b1 in Z )proof
assume
x in Z
;
x in (elementary_tree 1) with-replacement (<*0*>,(Z | z))
then reconsider x9 =
x as
Element of
Z ;
per cases
( x9 = {} or x9 <> {} )
;
suppose
x9 <> {}
;
x in (elementary_tree 1) with-replacement (<*0*>,(Z | z))then consider w being
FinSequence of
NAT ,
n being
Element of
NAT such that A6:
x9 = <*n*> ^ w
by FINSEQ_2:130;
<*n*> is_a_prefix_of x9
by A6, TREES_1:1;
then A7:
<*n*> in Z
by TREES_1:20;
<*n*> = (Root Z) ^ <*n*>
by FINSEQ_1:34;
then A8:
<*n*> in succ (Root Z)
by A7, TREES_2:12;
then
<*n*> = z
by A3, TARSKI:def 1;
then A9:
w in Z | z
by A6, TREES_1:def 6;
<*n*> = <*0*>
by A3, A4, A8, TARSKI:def 1;
hence
x in (elementary_tree 1) with-replacement (
<*0*>,
(Z | z))
by A1, A6, A9, TREES_1:def 9;
verum end; end;
end; assume
x in (elementary_tree 1) with-replacement (
<*0*>,
(Z | z))
;
b1 in Zthen reconsider x9 =
x as
Element of
(elementary_tree 1) with-replacement (
<*0*>,
(Z | z)) ;
end;
hence
Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z))
by TARSKI:2; verum