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