let I be non trivial finite set ; 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; 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; 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; 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; ( 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)
; 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; 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 ; 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; ( 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 )
; 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; verum