set f = NAT --> {};
reconsider f = NAT --> {} as ManySortedSet of NAT ;
take f ; :: thesis: for n being Nat holds f . n is AP:VLabeling of EL
let n be Nat; :: thesis: f . n is AP:VLabeling of EL
n in NAT by ORDINAL1:def 13;
then f . n = {} by FUNCOP_1:13;
then f . n is PartFunc of (the_Vertices_of G),({1} \/ (the_Edges_of G)) by RELSET_1:25;
hence f . n is AP:VLabeling of EL by Def5; :: thesis: verum