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

for O being connecting-mapping of CPNT

for q being connecting-firing-rule of O

for F being Function st F = union (rng q) holds

for g being Function

for x being object

for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x

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

for q being connecting-firing-rule of O

for F being Function st F = union (rng q) holds

for g being Function

for x being object

for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x

let O be connecting-mapping of CPNT; :: thesis: for q being connecting-firing-rule of O

for F being Function st F = union (rng q) holds

for g being Function

for x being object

for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x

let q be connecting-firing-rule of O; :: thesis: for F being Function st F = union (rng q) holds

for g being Function

for x being object

for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x

let F be Function; :: thesis: ( F = union (rng q) implies for g being Function

for x being object

for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x )

assume AS2: F = union (rng q) ; :: thesis: for g being Function

for x being object

for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x

let g be Function; :: thesis: for x being object

for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x

let x be object ; :: thesis: for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x

let i, j be Element of I; :: thesis: ( i <> j & g = q . [i,j] & x in dom g implies F . x = g . x )

assume A41: ( i <> j & g = q . [i,j] & x in dom g ) ; :: thesis: F . x = g . x

A42: [x,(g . x)] in q . [i,j] by A41, FUNCT_1:def 2;

[i,j] in XorDelta I by A41;

then [i,j] in dom q by PARTFUN1:def 2;

then q . [i,j] in rng q by FUNCT_1:3;

then A43: [x,(g . x)] in F by AS2, A42, TARSKI:def 4;

then x in dom F by XTUPLE_0:def 12;

hence g . x = F . x by A43, FUNCT_1:def 2; :: thesis: verum

for O being connecting-mapping of CPNT

for q being connecting-firing-rule of O

for F being Function st F = union (rng q) holds

for g being Function

for x being object

for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x

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

for q being connecting-firing-rule of O

for F being Function st F = union (rng q) holds

for g being Function

for x being object

for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x

let O be connecting-mapping of CPNT; :: thesis: for q being connecting-firing-rule of O

for F being Function st F = union (rng q) holds

for g being Function

for x being object

for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x

let q be connecting-firing-rule of O; :: thesis: for F being Function st F = union (rng q) holds

for g being Function

for x being object

for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x

let F be Function; :: thesis: ( F = union (rng q) implies for g being Function

for x being object

for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x )

assume AS2: F = union (rng q) ; :: thesis: for g being Function

for x being object

for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x

let g be Function; :: thesis: for x being object

for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x

let x be object ; :: thesis: for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds

F . x = g . x

let i, j be Element of I; :: thesis: ( i <> j & g = q . [i,j] & x in dom g implies F . x = g . x )

assume A41: ( i <> j & g = q . [i,j] & x in dom g ) ; :: thesis: F . x = g . x

A42: [x,(g . x)] in q . [i,j] by A41, FUNCT_1:def 2;

[i,j] in XorDelta I by A41;

then [i,j] in dom q by PARTFUN1:def 2;

then q . [i,j] in rng q by FUNCT_1:3;

then A43: [x,(g . x)] in F by AS2, A42, TARSKI:def 4;

then x in dom F by XTUPLE_0:def 12;

hence g . x = F . x by A43, FUNCT_1:def 2; :: thesis: verum