let I be non trivial finite set ; :: thesis: for CPNT being Colored-PT-net-Family of I st CPNT is disjoint_valued holds

for O being connecting-mapping of CPNT

for q being connecting-firing-rule of O st ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st

( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds

j1 = j2 ) holds

( union (rng q) is Function & ( for z being object st z in union (rng q) holds

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) )

let CPNT be Colored-PT-net-Family of I; :: thesis: ( CPNT is disjoint_valued implies for O being connecting-mapping of CPNT

for q being connecting-firing-rule of O st ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st

( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds

j1 = j2 ) holds

( union (rng q) is Function & ( for z being object st z in union (rng q) holds

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) ) )

assume AS0: CPNT is disjoint_valued ; :: thesis: for O being connecting-mapping of CPNT

for q being connecting-firing-rule of O st ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st

( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds

j1 = j2 ) holds

( union (rng q) is Function & ( for z being object st z in union (rng q) holds

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) )

let O be connecting-mapping of CPNT; :: thesis: for q being connecting-firing-rule of O st ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st

( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds

j1 = j2 ) holds

( union (rng q) is Function & ( for z being object st z in union (rng q) holds

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) )

let q be connecting-firing-rule of O; :: thesis: ( ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st

( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds

j1 = j2 ) implies ( union (rng q) is Function & ( for z being object st z in union (rng q) holds

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) ) )

assume AS1: for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st

( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds

j1 = j2 ; :: thesis: ( union (rng q) is Function & ( for z being object st z in union (rng q) holds

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) )

E1: for RQ being object st RQ in rng q holds

ex i, j being Element of I ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) & qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & RQ = q . [i,j] & q . [i,j] = qij & O . [i,j] = Oij )

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 )

ex x, y being object st z = [x,y]

for x, y1, y2 being object st [x,y1] in G1 & [x,y2] in G1 holds

y1 = y2

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) ) by E5, FUNCT_1:def 1; :: thesis: verum

for O being connecting-mapping of CPNT

for q being connecting-firing-rule of O st ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st

( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds

j1 = j2 ) holds

( union (rng q) is Function & ( for z being object st z in union (rng q) holds

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) )

let CPNT be Colored-PT-net-Family of I; :: thesis: ( CPNT is disjoint_valued implies for O being connecting-mapping of CPNT

for q being connecting-firing-rule of O st ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st

( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds

j1 = j2 ) holds

( union (rng q) is Function & ( for z being object st z in union (rng q) holds

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) ) )

assume AS0: CPNT is disjoint_valued ; :: thesis: for O being connecting-mapping of CPNT

for q being connecting-firing-rule of O st ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st

( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds

j1 = j2 ) holds

( union (rng q) is Function & ( for z being object st z in union (rng q) holds

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) )

let O be connecting-mapping of CPNT; :: thesis: for q being connecting-firing-rule of O st ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st

( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds

j1 = j2 ) holds

( union (rng q) is Function & ( for z being object st z in union (rng q) holds

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) )

let q be connecting-firing-rule of O; :: thesis: ( ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st

( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds

j1 = j2 ) implies ( union (rng q) is Function & ( for z being object st z in union (rng q) holds

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) ) )

assume AS1: for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st

( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds

j1 = j2 ; :: thesis: ( union (rng q) is Function & ( for z being object st z in union (rng q) holds

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) )

E1: for RQ being object st RQ in rng q holds

ex i, j being Element of I ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) & qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & RQ = q . [i,j] & q . [i,j] = qij & O . [i,j] = Oij )

proof

E5:
for z being object st z in union (rng q) holds
let RQ be object ; :: thesis: ( RQ in rng q implies ex i, j being Element of I ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) & qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & RQ = q . [i,j] & q . [i,j] = qij & O . [i,j] = Oij ) )

assume RQ in rng q ; :: thesis: ex i, j being Element of I ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) & qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & RQ = q . [i,j] & q . [i,j] = qij & O . [i,j] = Oij )

then consider z being object such that

E2: ( z in dom q & RQ = q . z ) by FUNCT_1:def 3;

z in XorDelta I by E2;

then consider i, j being Element of I such that

E3: ( z = [i,j] & i <> j ) ;

consider Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j), qij being Function such that

E4: ( qij = q . [i,j] & Oij = O . [i,j] & dom qij = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) ) by E3, Defcntfir;

qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) by SYLM3, E4;

hence ex i, j being Element of I ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) & qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & RQ = q . [i,j] & q . [i,j] = qij & O . [i,j] = Oij ) by E2, E3, E4; :: thesis: verum

end;( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) & qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & RQ = q . [i,j] & q . [i,j] = qij & O . [i,j] = Oij ) )

assume RQ in rng q ; :: thesis: ex i, j being Element of I ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) & qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & RQ = q . [i,j] & q . [i,j] = qij & O . [i,j] = Oij )

then consider z being object such that

E2: ( z in dom q & RQ = q . z ) by FUNCT_1:def 3;

z in XorDelta I by E2;

then consider i, j being Element of I such that

E3: ( z = [i,j] & i <> j ) ;

consider Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j), qij being Function such that

E4: ( qij = q . [i,j] & Oij = O . [i,j] & dom qij = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) ) by E3, Defcntfir;

qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) by SYLM3, E4;

hence ex i, j being Element of I ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) & qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & RQ = q . [i,j] & q . [i,j] = qij & O . [i,j] = Oij ) by E2, E3, E4; :: thesis: verum

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 )

proof

for z being object st z in union (rng q) holds
let z be object ; :: thesis: ( z in union (rng q) implies ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) )

assume z in union (rng q) ; :: thesis: ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 )

then consider Z being set such that

E6: ( z in Z & Z in rng q ) by TARSKI:def 4;

consider i, j being Element of I, Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j), qij being Function such that

E8: ( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) & qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & Z = q . [i,j] & q . [i,j] = qij & O . [i,j] = Oij ) by E1, E6;

thus ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) by E6, E8; :: thesis: verum

end;( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) )

assume z in union (rng q) ; :: thesis: ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 )

then consider Z being set such that

E6: ( z in Z & Z in rng q ) by TARSKI:def 4;

consider i, j being Element of I, Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j), qij being Function such that

E8: ( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) & qij in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & Z = q . [i,j] & q . [i,j] = qij & O . [i,j] = Oij ) by E1, E6;

thus ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) by E6, E8; :: thesis: verum

ex x, y being object st z = [x,y]

proof

then reconsider G1 = union (rng q) as Relation by RELAT_1:def 1;
let z be object ; :: thesis: ( z in union (rng q) implies ex x, y being object st z = [x,y] )

assume z in union (rng q) ; :: thesis: ex x, y being object st z = [x,y]

then consider i, j being Element of I, q12 being Function, O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) such that

U1: ( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) by E5;

thus ex x, y being object st z = [x,y] by U1, RELAT_1:def 1; :: thesis: verum

end;assume z in union (rng q) ; :: thesis: ex x, y being object st z = [x,y]

then consider i, j being Element of I, q12 being Function, O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) such that

U1: ( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) by E5;

thus ex x, y being object st z = [x,y] by U1, RELAT_1:def 1; :: thesis: verum

for x, y1, y2 being object st [x,y1] in G1 & [x,y2] in G1 holds

y1 = y2

proof

hence
( union (rng q) is Function & ( for z being object st z in union (rng q) holds
let x, y1, y2 be object ; :: thesis: ( [x,y1] in G1 & [x,y2] in G1 implies y1 = y2 )

assume P01: ( [x,y1] in G1 & [x,y2] in G1 ) ; :: thesis: y1 = y2

then consider i1, j1 being Element of I, q121 being Function, O121 being Function of (Outbds (CPNT . i1)), the carrier of (CPNT . j1) such that

U11: ( i1 <> j1 & ( for t01 being transition of (CPNT . i1) st t01 is outbound holds

q121 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i1),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i1),(Im (O121,t01)))) ) & q121 in Funcs ((Outbds (CPNT . i1)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i1),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i1),(Im (O121,t01)))))) where t01 is transition of (CPNT . i1) : t01 is outbound } )) & q121 = q . [i1,j1] & O121 = O . [i1,j1] & [x,y1] in q121 ) by E5;

consider i2, j2 being Element of I, q122 being Function, O122 being Function of (Outbds (CPNT . i2)), the carrier of (CPNT . j2) such that

U12: ( i2 <> j2 & ( for t01 being transition of (CPNT . i2) st t01 is outbound holds

q122 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i2),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i2),(Im (O122,t01)))) ) & q122 in Funcs ((Outbds (CPNT . i2)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i2),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i2),(Im (O122,t01)))))) where t01 is transition of (CPNT . i2) : t01 is outbound } )) & q122 = q . [i2,j2] & O122 = O . [i2,j2] & [x,y2] in q122 ) by E5, P01;

x in dom q121 by U11, XTUPLE_0:def 12;

then s1: x in Outbds (CPNT . i1) by U11, FUNCT_2:92;

x in dom q122 by U12, XTUPLE_0:def 12;

then s2: x in Outbds (CPNT . i2) by U12, FUNCT_2:92;

i1 = i2

hence y1 = y2 by U11, FUNCT_1:def 1; :: thesis: verum

end;assume P01: ( [x,y1] in G1 & [x,y2] in G1 ) ; :: thesis: y1 = y2

then consider i1, j1 being Element of I, q121 being Function, O121 being Function of (Outbds (CPNT . i1)), the carrier of (CPNT . j1) such that

U11: ( i1 <> j1 & ( for t01 being transition of (CPNT . i1) st t01 is outbound holds

q121 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i1),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i1),(Im (O121,t01)))) ) & q121 in Funcs ((Outbds (CPNT . i1)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i1),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i1),(Im (O121,t01)))))) where t01 is transition of (CPNT . i1) : t01 is outbound } )) & q121 = q . [i1,j1] & O121 = O . [i1,j1] & [x,y1] in q121 ) by E5;

consider i2, j2 being Element of I, q122 being Function, O122 being Function of (Outbds (CPNT . i2)), the carrier of (CPNT . j2) such that

U12: ( i2 <> j2 & ( for t01 being transition of (CPNT . i2) st t01 is outbound holds

q122 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i2),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i2),(Im (O122,t01)))) ) & q122 in Funcs ((Outbds (CPNT . i2)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i2),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i2),(Im (O122,t01)))))) where t01 is transition of (CPNT . i2) : t01 is outbound } )) & q122 = q . [i2,j2] & O122 = O . [i2,j2] & [x,y2] in q122 ) by E5, P01;

x in dom q121 by U11, XTUPLE_0:def 12;

then s1: x in Outbds (CPNT . i1) by U11, FUNCT_2:92;

x in dom q122 by U12, XTUPLE_0:def 12;

then s2: x in Outbds (CPNT . i2) by U12, FUNCT_2:92;

i1 = i2

proof

then
[x,y2] in q121
by U12, U11, AS1;
assume
i1 <> i2
; :: thesis: contradiction

then the carrier' of (CPNT . i1) /\ the carrier' of (CPNT . i2) = {} by AS0, XBOOLE_0:def 7;

hence contradiction by XBOOLE_0:def 4, s1, s2; :: thesis: verum

end;then the carrier' of (CPNT . i1) /\ the carrier' of (CPNT . i2) = {} by AS0, XBOOLE_0:def 7;

hence contradiction by XBOOLE_0:def 4, s1, s2; :: thesis: verum

hence y1 = y2 by U11, FUNCT_1:def 1; :: thesis: verum

ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st

( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds

q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) ) by E5, FUNCT_1:def 1; :: thesis: verum