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

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