deffunc H1( 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 H1(i,j)
proof
let i, j be Element of I; :: thesis: 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 H1(i,j)

let Oij be Function of (Outbds (CPNT . i)), the carrier of (CPNT . j); :: thesis: 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 H1(i,j)

let q be Function; :: thesis: ( 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)))) ) implies q in union H1(i,j) )

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: q in union H1(i,j)
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 ;
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 H1(i,j) by A1;
hence q in union H1(i,j) by ; :: thesis: verum
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 ;
reconsider Oj0i0 = O . [j0,i0] as Function of (Outbds (CPNT . j0)), the carrier of (CPNT . i0) by ;
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 H1(i0,j0) in { (union H1(i,j)) where i, j is Element of I : i <> j } by I0J0;
then union H1(i0,j0) c= union { (union H1(i,j)) where i, j is Element of I : i <> j } by ZFMISC_1:74;
then reconsider Y = union { (union H1(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: 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

let Oij be Function of (Outbds (CPNT . i)), the carrier of (CPNT . j); :: thesis: 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

let q be Function; :: thesis: ( 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)))) ) implies q in Y )

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: q in Y
then A2: q in union H1(i,j) by R1;
union H1(i,j) in { (union H1(i,j)) where i, j is Element of I : i <> j } by A1;
hence q in Y by ; :: thesis: verum
end;
defpred S1[ 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 & S1[x,y] )
proof
let x be object ; :: thesis: ( x in XorDelta I implies ex y being object st
( y in Y & S1[x,y] ) )

assume x in XorDelta I ; :: thesis: ex y being object st
( y in Y & S1[x,y] )

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 ;
reconsider Oji = O . [j,i] as Function of (Outbds (CPNT . j)), the carrier of (CPNT . i) by ;
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 & S1[x,y] ) by X0, P11, R2; :: thesis: verum
end;
consider f being Function of (),Y such that
P2: for x being object st x in XorDelta I holds
S1[x,f . x] from reconsider f = f as ManySortedSet of XorDelta I ;
take f ; :: thesis: 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)))) ) )

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: verum
proof
let i, j be Element of I; :: thesis: ( i <> j implies 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)))) ) ) )

assume i <> j ; :: thesis: 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)))) ) )

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 ;
( i = i1 & j = j1 ) by ;
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: verum
end;