:: deftheorem Def19 defines FF:ELabelingSeq GLIB_005:def 19 :
for G being _Graph
for b₂ being ManySortedSet of NAT holds
( b₂ is FF:ELabelingSeq of G iff for n being Nat holds b₂ . n is FF:ELabeling of G );