consider G being finite Tree-like _Graph;
set F = NAT --> G;
A1: dom (NAT --> G) = NAT by FUNCOP_1:19;
reconsider F = NAT --> G as ManySortedSet of ;

now

let x be Nat; :: thesis: F . x is _Graph
x in NAT by ORDINAL1:def 13;
then F . x in rng F by A1, FUNCT_1:12;
then F . x in {G} by FUNCOP_1:14;
hence F . x is _Graph by TARSKI:def 1; :: thesis: verum

end;

then reconsider F = F as GraphSeq by GLIB_000:def 55;
take F ; :: thesis: ( F is halting & F is finite & F is Tree-like )
( F . 1 in rng F & F . (1 + 1) in rng F ) by A1, FUNCT_1:12;
then ( F . 1 in {G} & F . (1 + 1) in {G} ) by FUNCOP_1:14;
then ( F . 1 = G & F . (1 + 1) = G ) by TARSKI:def 1;
hence F is halting by GLIB_000:def 56; :: thesis: ( F is finite & F is Tree-like )

now

let x be Nat; :: thesis: ( F . x is finite & F . x is Tree-like )
x in NAT by ORDINAL1:def 13;
then F . x in rng F by A1, FUNCT_1:12;
then F . x in {G} by FUNCOP_1:14;
hence ( F . x is finite & F . x is Tree-like ) by TARSKI:def 1; :: thesis: verum

end;

hence ( F is finite & F is Tree-like ) by Def14, GLIB_000:def 60; :: thesis: verum