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
f . n = {} ;
then f . n is PartFunc of (the_Vertices_of G),({1} \/ (the_Edges_of G)) by RELSET_1:12;
hence f . n is AP:VLabeling of EL by Def5; :: thesis: verum