let I be non trivial finite set ; :: thesis: for CPNT being Colored-PT-net-Family of I
for N being Function of I,(bool (rng CPNT))
for O being connecting-mapping of CPNT st CPNT is one-to-one & N,O is_Cell-Petri-nets holds
for i being Element of I holds not CPNT . i in N . i
let CPNT be Colored-PT-net-Family of I; :: thesis: for N being Function of I,(bool (rng CPNT))
for O being connecting-mapping of CPNT st CPNT is one-to-one & N,O is_Cell-Petri-nets holds
for i being Element of I holds not CPNT . i in N . i
let N be Function of I,(bool (rng CPNT)); :: thesis: for O being connecting-mapping of CPNT st CPNT is one-to-one & N,O is_Cell-Petri-nets holds
for i being Element of I holds not CPNT . i in N . i
let O be connecting-mapping of CPNT; :: thesis: ( CPNT is one-to-one & N,O is_Cell-Petri-nets implies for i being Element of I holds not CPNT . i in N . i )
assume A1: CPNT is one-to-one ; :: thesis: ( not N,O is_Cell-Petri-nets or for i being Element of I holds not CPNT . i in N . i )
assume A2: N,O is_Cell-Petri-nets ; :: thesis: for i being Element of I holds not CPNT . i in N . i
let i be Element of I; :: thesis: not CPNT . i in N . i
assume A3: CPNT . i in N . i ; :: thesis: contradiction
N . i = { (CPNT . j) where j is Element of I : ( j <> i & ex t being transition of (CPNT . i) ex s being object st [t,s] in O . [i,j] ) } by A2;
then consider j being Element of I such that
A4: ( CPNT . i = CPNT . j & j <> i & ex t being transition of (CPNT . i) ex s being object st [t,s] in O . [i,j] ) by A3;
dom CPNT = I by PARTFUN1:def 2;
hence contradiction by A1, A4, FUNCT_1:def 4; :: thesis: verum