deffunc H₁( Element of I, Element of I) -> set = { (Funcs ((Outbds (CPNT . $1)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . $1),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . $1),(Im (O12,t01)))))) where t01 is transition of (CPNT . $1) : t01 is outbound } ))) where O12 is Function of (Outbds (CPNT . $1)), the carrier of (CPNT . $2) : O . [$1,$2] = O12 } ;
R1: for i, j being Element of I
for Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j)
for q being Function st Oij = O . [i,j] & dom q = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
q . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) holds
q in union H₁(i,j)

proof

let i, j be Element of I; :: thesis:
let Oij be Function of (Outbds (CPNT . i)), the carrier of (CPNT . j); :: thesis:
let q be Function; :: thesis:
assume A1: ( Oij = O . [i,j] & dom q = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
q . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) ) ; :: thesis:
P1: q 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, A1;
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 } )) in H₁(i,j) by A1;
hence q in union H₁(i,j) by P1, TARSKI:def 4; :: thesis:

end;

consider i0, j0 being Element of I such that
I0J0: i0 <> j0 by LMXorDelta;
reconsider Oi0j0 = O . [i0,j0] as Function of (Outbds (CPNT . i0)), the carrier of (CPNT . j0) by I0J0, Defcntmap;
reconsider Oj0i0 = O . [j0,i0] as Function of (Outbds (CPNT . j0)), the carrier of (CPNT . i0) by I0J0, Defcntmap;
reconsider O0 = [Oi0j0,Oj0i0] as connecting-mapping of CPNT . i0,CPNT . j0 by PETRI_2:def 13;
set q0 = the connecting-firing-rule of CPNT . i0,CPNT . j0,O0;
consider q12, q21 being Function, O12 being Function of (Outbds (CPNT . i0)), the carrier of (CPNT . j0), O21 being Function of (Outbds (CPNT . j0)), the carrier of (CPNT . i0) such that
X0: ( O0 = [O12,O21] & dom q12 = Outbds (CPNT . i0) & dom q21 = Outbds (CPNT . j0) & ( for t01 being transition of (CPNT . i0) st t01 is outbound holds
q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i0),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i0),(Im (O12,t01)))) ) & ( for t02 being transition of (CPNT . j0) st t02 is outbound holds
q21 . t02 is Function of (thin_cylinders ( the ColoredSet of (CPNT . j0),(*' {t02}))),(thin_cylinders ( the ColoredSet of (CPNT . j0),(Im (O21,t02)))) ) & the connecting-firing-rule of CPNT . i0,CPNT . j0,O0 = [q12,q21] ) by PETRI_2:def 14;
x1: Oi0j0 = O0 `1
.= O12 by X0 ;
union H₁(i0,j0) in { (union H₁(i,j)) where i, j is Element of I : i <> j } by I0J0;
then union H₁(i0,j0) c= union { (union H₁(i,j)) where i, j is Element of I : i <> j } by ZFMISC_1:74;
then reconsider Y = union { (union H₁(i,j)) where i, j is Element of I : i <> j } as non empty set by x1, X0, R1;
R2: for i, j being Element of I
for Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j)
for q being Function st i <> j & Oij = O . [i,j] & dom q = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
q . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) holds
q in Y

proof

let i, j be Element of I; :: thesis:
let Oij be Function of (Outbds (CPNT . i)), the carrier of (CPNT . j); :: thesis:
let q be Function; :: thesis:
assume A1: ( i <> j & Oij = O . [i,j] & dom q = Outbds (CPNT . i) & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
q . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) ) ; :: thesis:
then A2: q in union H₁(i,j) by R1;
union H₁(i,j) in { (union H₁(i,j)) where i, j is Element of I : i <> j } by A1;
hence q in Y by A2, TARSKI:def 4; :: thesis:

end;

defpred S₁[ object , object ] means 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
( $1 = [i,j] & Oij = O . [i,j] & qij = $2 & 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)))) ) );
P1: for x being object st x in XorDelta I holds
ex y being object st
( y in Y & S₁[x,y] )

proof

let x be object ; :: thesis:
assume x in XorDelta I ; :: thesis:
then consider i, j being Element of I such that
P11: ( x = [i,j] & i <> j ) ;
reconsider Oij = O . [i,j] as Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) by P11, Defcntmap;
reconsider Oji = O . [j,i] as Function of (Outbds (CPNT . j)), the carrier of (CPNT . i) by P11, Defcntmap;
reconsider O0 = [Oij,Oji] as connecting-mapping of CPNT . i,CPNT . j by PETRI_2:def 13;
set q0 = the connecting-firing-rule of CPNT . i,CPNT . j,O0;
consider q12, q21 being Function, O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j), O21 being Function of (Outbds (CPNT . j)), the carrier of (CPNT . i) such that
X0: ( O0 = [O12,O21] & dom q12 = Outbds (CPNT . i) & dom q21 = Outbds (CPNT . 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)))) ) & ( for t02 being transition of (CPNT . j) st t02 is outbound holds
q21 . t02 is Function of (thin_cylinders ( the ColoredSet of (CPNT . j),(*' {t02}))),(thin_cylinders ( the ColoredSet of (CPNT . j),(Im (O21,t02)))) ) & the connecting-firing-rule of CPNT . i,CPNT . j,O0 = [q12,q21] ) by PETRI_2:def 14;
Oij = O0 `1
.= O12 by X0 ;
hence ex y being object st
( y in Y & S₁[x,y] ) by X0, P11, R2; :: thesis:

end;

consider f being Function of (XorDelta I),Y such that
P2: for x being object st x in XorDelta I holds
S₁[x,f . x] from FUNCT_2:sch 1(P1);
reconsider f = f as ManySortedSet of XorDelta I ;
take f ; :: thesis:
thus for i, j being Element of I st i <> j holds
ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st
( qij = f . [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)))) ) ) :: thesis:

proof

let i, j be Element of I; :: thesis:
assume i <> j ; :: thesis:
then p04: [i,j] in XorDelta I ;
consider i1, j1 being Element of I, Oij being Function of (Outbds (CPNT . i1)), the carrier of (CPNT . j1), qij being Function such that
P4: ( [i,j] = [i1,j1] & Oij = O . [i1,j1] & qij = f . [i,j] & i1 <> j1 & dom qij = Outbds (CPNT . i1) & ( for t01 being transition of (CPNT . i1) st t01 is outbound holds
qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i1),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i1),(Im (Oij,t01)))) ) ) by p04, P2;
( i = i1 & j = j1 ) by XTUPLE_0:1, P4;
hence ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st
( qij = f . [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 P4; :: thesis:

end;