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 by FUNCOP_1:13;
reconsider F = NAT --> the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph as ManySortedSet of NAT ;

now

let x be Nat; :: thesis: F . x is _Graph
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 _Graph by TARSKI:def 1; :: thesis: verum

end;

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

now

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

end;

then reconsider F = F as [Weighted] [ELabeled] [VLabeled] GraphSeq by Def24, Def25, Def26;
F . (1 + 1) in rng F by A1, FUNCT_1:3;
then F . (1 + 1) in { the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph} by FUNCOP_1:8;
then A2: F . (1 + 1) = the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph by TARSKI:def 1;
take F ; :: thesis: ( F is halting & 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 )
F . 1 in rng F by A1, FUNCT_1:3;
then F . 1 in { the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph} by FUNCOP_1:8;
then F . 1 = the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph by TARSKI:def 1;
hence F is halting by A2, GLIB_000:def 54; :: thesis: ( 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 )

now

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

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 57, GLIB_000:def 58, GLIB_000:def 59, GLIB_000:def 61, GLIB_000:def 63, GLIB_002:def 14; :: thesis: verum