set G = the _finite Tree-like _Graph;

set F = NAT --> the _finite Tree-like _Graph;

A1: dom (NAT --> the _finite Tree-like _Graph) = NAT ;

reconsider F = NAT --> the _finite Tree-like _Graph as ManySortedSet of NAT ;

reconsider F = F as GraphSeq ;

A2: F . (1 + 1) = the _finite Tree-like _Graph ;

take F ; :: thesis: ( F is halting & F is _finite & F is Tree-like )

F . 1 = the _finite Tree-like _Graph ;

hence F is halting by A2, GLIB_000:def 55; :: thesis: ( F is _finite & F is Tree-like )

set F = NAT --> the _finite Tree-like _Graph;

A1: dom (NAT --> the _finite Tree-like _Graph) = NAT ;

reconsider F = NAT --> the _finite Tree-like _Graph as ManySortedSet of NAT ;

reconsider F = F as GraphSeq ;

A2: F . (1 + 1) = the _finite Tree-like _Graph ;

take F ; :: thesis: ( F is halting & F is _finite & F is Tree-like )

F . 1 = the _finite Tree-like _Graph ;

hence F is halting by A2, GLIB_000:def 55; :: thesis: ( F is _finite & F is Tree-like )

now :: thesis: for x being Nat holds

( F . x is _finite & F . x is Tree-like )

hence
( F is _finite & F is Tree-like )
by GLIB_000:def 74; :: thesis: verum( F . x is _finite & F . x is Tree-like )

let x be Nat; :: thesis: ( F . x is _finite & F . x is Tree-like )

x in NAT by ORDINAL1:def 12;

then F . x in rng F by A1, FUNCT_1:3;

then F . x in { the _finite Tree-like _Graph} by FUNCOP_1:8;

hence ( F . x is _finite & F . x is Tree-like ) by TARSKI:def 1; :: thesis: verum

end;x in NAT by ORDINAL1:def 12;

then F . x in rng F by A1, FUNCT_1:3;

then F . x in { the _finite Tree-like _Graph} by FUNCOP_1:8;

hence ( F . x is _finite & F . x is Tree-like ) by TARSKI:def 1; :: thesis: verum