:: deftheorem Def11 defines AP:VLabelingSeq GLIB_005:def 11 :
for G being _Graph
for EL being FF:ELabeling of G
for b₃ being ManySortedSet of NAT holds
( b₃ is AP:VLabelingSeq of EL iff for n being Nat holds b₃ . n is AP:VLabeling of EL );