:: deftheorem Defcntmap defines connecting-mapping PETRI_3:def 4 :
for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I
for b₃ being ManySortedSet of XorDelta I holds
( b₃ is connecting-mapping of CPNT iff ( rng b₃ c= union { (Funcs ((Outbds (CPNT . i)), the carrier of (CPNT . j))) where i, j is Element of I : i <> j } & ( for i, j being Element of I st i <> j holds
b₃ . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ) ) );