set G = the _finite loopless _trivial non-multi simple nonnegative-weighted real-WEV WEVGraph;
set F = NAT --> the _finite loopless _trivial non-multi simple nonnegative-weighted real-WEV WEVGraph;
A1: dom (NAT --> the _finite loopless _trivial non-multi simple nonnegative-weighted real-WEV WEVGraph) = NAT ;
reconsider F = NAT --> the _finite loopless _trivial non-multi simple nonnegative-weighted real-WEV WEVGraph as ManySortedSet of NAT ;
reconsider F = F as GraphSeq ;
take F ; :: thesis: ( F is [Weighted] & F is [ELabeled] & F is [VLabeled] )

now :: thesis: for x being Nat holds
( F . x is [Weighted] & F . x is [ELabeled] & F . x is [VLabeled] )

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 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;

hence ( F is [Weighted] & F is [ELabeled] & F is [VLabeled] ) ; :: thesis: verum