consider G being finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph;
set F = NAT --> G;
A1: dom (NAT --> G) = NAT by FUNCOP_1:19;
reconsider F = NAT --> G as ManySortedSet of ;

let x be Nat; :: thesis:
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:

end;

then reconsider F = F as GraphSeq by GLIB_000:def 55;

let x be Nat; :: thesis:
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 [Weighted] & F . x is [ELabeled] & F . x is [VLabeled] ) by TARSKI:def 1; :: thesis:

end;

then reconsider F = F as [Weighted] [ELabeled] [VLabeled] GraphSeq by Def24, Def25, Def26;
take F ; :: thesis:
( 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:

let x be Nat; :: thesis:
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 loopless & F . x is trivial & F . x is non-multi & F . x is simple & F . x is real-WEV & F . x is nonnegative-weighted & F . x is Tree-like ) by TARSKI:def 1; :: thesis:

end;

hence ( F is finite & F is loopless & F is trivial & F is non-multi & F is simple & F is real-WEV & F is nonnegative-weighted & F is Tree-like ) by Def28, Def31, GLIB_000:def 60, GLIB_000:def 61, GLIB_000:def 62, GLIB_000:def 64, GLIB_000:def 66, GLIB_002:def 14; :: thesis: