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 )
proof
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 ;
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 ;
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;
E5: 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 )
proof
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;
for z being object st z in union (rng q) holds
ex x, y being object st z = [x,y]
proof
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 ; :: thesis: verum
end;
then reconsider G1 = union (rng q) as Relation by RELAT_1:def 1;
for x, y1, y2 being object st [x,y1] in G1 & [x,y2] in G1 holds
y1 = y2
proof
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 ;
x in dom q121 by ;
then s1: x in Outbds (CPNT . i1) by ;
x in dom q122 by ;
then s2: x in Outbds (CPNT . i2) by ;
i1 = i2
proof
assume i1 <> i2 ; :: thesis: contradiction
then the carrier' of (CPNT . i1) /\ the carrier' of (CPNT . i2) = {} by ;
hence contradiction by XBOOLE_0:def 4, s1, s2; :: thesis: verum
end;
then [x,y2] in q121 by ;
hence y1 = y2 by ; :: thesis: verum
end;
hence ( 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 ) ) ) by ; :: thesis: verum