:: deftheorem Def12 defines Enumeration PETRI_DF:def 1 :
for X being set
for Y being non empty set
for P being finite Subset of X
for M0 being Function of X,Y
for b₅ being FinSequence of Y holds
( ( not P is empty implies ( b₅ is Enumeration of M0,P iff ( len b₅ = len the Enumeration of P & ( for i being Nat st i in dom b₅ holds
b₅ . i = M0 . ( the Enumeration of P . i) ) ) ) ) & ( P is empty implies ( b₅ is Enumeration of M0,P iff b₅ = <*> Y ) ) );