let t be Tree; :: thesis: ( t is finite implies t is finite-order )
assume t is finite ; :: thesis: t is finite-order
then reconsider s = t as finite Tree ;
take n = (card s) + 1; :: according to TREES_2:def 2 :: thesis: for b₁ being Element of t holds not b₁ ^ <*n*> in t
let x be Element of t; :: thesis: not x ^ <*n*> in t
assume A1: x ^ <*n*> in t ; :: thesis: contradiction
deffunc H₁( Nat) -> set = x ^ <*(c₁ - 1)*>;
consider f being FinSequence such that
A2: ( len f = n & ( for i being Nat st i in dom f holds
f . i = H₁(i) ) ) from FINSEQ_1:sch 2();
A4: dom f = Seg n by A2, FINSEQ_1:def 3;
A5: rng f c= succ x

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in succ x )
assume y in rng f ; :: thesis: y in succ x
then consider i being set such that
A6: ( i in dom f & y = f . i ) by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A6;
A7: ( i >= 1 & i <= n ) by A4, A6, FINSEQ_1:3;
then consider j being Nat such that
A8: i = 1 + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
j <= i by A8, NAT_1:11;
then ( i - 1 = j & j <= n ) by A7, A8, XXREAL_0:2;
then ( y = x ^ <*j*> & x ^ <*j*> in t ) by A1, A2, A6, TREES_1:def 5;
hence y in succ x ; :: thesis: verum

end;

f is one-to-one

proof

let z, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not z in dom f or not y in dom f or not f . z = f . y or z = y )
assume A9: ( z in dom f & y in dom f & f . z = f . y ) ; :: thesis: z = y
then reconsider i1 = z, i2 = y as Element of NAT ;
( f . z = x ^ <*(i1 - 1)*> & f . y = x ^ <*(i2 - 1)*> ) by A2, A9;
then <*(i1 - 1)*> = <*(i2 - 1)*> by A9, FINSEQ_1:46;
then i1 - 1 = <*(i2 - 1)*> . 1 by FINSEQ_1:57
.= i2 - 1 by FINSEQ_1:57 ;
hence z = y ; :: thesis: verum

end;

then ( card (dom f) c= card (succ x) & card (succ x) c= card t ) by A5, CARD_1:26, CARD_1:27;
then ( card (dom f) c= card t & card (Seg n) = n ) by FINSEQ_1:78, XBOOLE_1:1;
then ( n <= card s & card s <= n ) by A4, NAT_1:11, NAT_1:40;
then n = (card s) + 0 by XXREAL_0:1;
hence contradiction ; :: thesis: verum