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
deffunc H₁( Nat) -> set = x ^ <*(c₁ - 1)*>;
consider f being FinSequence such that
A1: ( len f = n & ( for i being Nat st i in dom f holds
f . i = H₁(i) ) ) from FINSEQ_1:sch 2();
A2: dom f = Seg n by A1, FINSEQ_1:def 3;
assume A3: x ^ <*n*> in t ; :: thesis: contradiction
A4: rng f c= succ x

proof

let y be object ; :: 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 object such that
A5: i in dom f and
A6: y = f . i by FUNCT_1:def 3;
reconsider i = i as Nat by A5;
i >= 1 by A2, A5, FINSEQ_1:1;
then consider j being Nat such that
A7: i = 1 + j by NAT_1:10;
reconsider j = j as Nat ;
A8: j <= i by A7, NAT_1:11;
i <= n by A2, A5, FINSEQ_1:1;
then j <= n by A8, XXREAL_0:2;
then A9: x ^ <*j*> in t by A3, TREES_1:def 3;
i - 1 = j by A7;
then y = x ^ <*j*> by A1, A5, A6;
hence y in succ x by A9; :: thesis: verum

end;

A10: card (succ x) c= card t by CARD_1:11;
f is one-to-one

proof

let z, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not z in proj1 f or not y in proj1 f or not f . z = f . y or z = y )
assume that
A11: ( z in dom f & y in dom f ) and
A12: f . z = f . y ; :: thesis: z = y
reconsider i1 = z, i2 = y as Nat by A11;
( f . z = x ^ <*(i1 - 1)*> & f . y = x ^ <*(i2 - 1)*> ) by A1, A11;
then <*(i1 - 1)*> = <*(i2 - 1)*> by A12, FINSEQ_1:33;
then i1 - 1 = <*(i2 - 1)*> . 1
.= i2 - 1 ;
hence z = y ; :: thesis: verum

end;

then card (dom f) c= card (succ x) by A4, CARD_1:10;
then A13: Segm (card (dom f)) c= Segm (card s) by A10;
A14: card s <= n by NAT_1:11;
card (Seg n) = n by FINSEQ_1:57;
then n <= card s by A2, A13, NAT_1:39;
then n = (card s) + 0 by A14, XXREAL_0:1;
hence contradiction ; :: thesis: verum