:: deftheorem Def13 defines connecting-mapping PETRI_2:def 13 :
for CPNT1, CPNT2 being Colored_Petri_net
for b₃ being set holds
( b₃ is connecting-mapping of CPNT1,CPNT2 iff ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st b₃ = [O12,O21] );