set G = the _finite loopless _trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph;
set F = NAT --> the _finite loopless _trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph;
A1: dom (NAT --> the _finite loopless _trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph) = NAT ;
reconsider F = NAT --> the _finite loopless _trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph as ManySortedSet of NAT ;
reconsider F = F as GraphSeq ;

let x be Nat; :: thesis:
x in NAT by ORDINAL1:def 12;
then F . x in rng F by A1, FUNCT_1:3;
then F . x in { the _finite loopless _trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph} by FUNCOP_1:8;
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;
A2: F . (1 + 1) = the _finite loopless _trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph ;
take F ; :: thesis:
F . 1 = the _finite loopless _trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph ;
hence F is halting by A2; :: thesis:

let x be Nat; :: thesis:
x in NAT by ORDINAL1:def 12;
then F . x in rng F by A1, FUNCT_1:3;
then F . x in { the _finite loopless _trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph} by FUNCOP_1:8;
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 GLIB_002:def 20; :: thesis: