deffunc H_{1}( 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_{1}(i,j)

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_{1}(i0,j0) in { (union H_{1}(i,j)) where i, j is Element of I : i <> j }
by I0J0;

then union H_{1}(i0,j0) c= union { (union H_{1}(i,j)) where i, j is Element of I : i <> j }
by ZFMISC_1:74;

then reconsider Y = union { (union H_{1}(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_{1}[ 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_{1}[x,y] )

P2: for x being object st x in XorDelta I holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(P1);

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

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

proof

consider i0, j0 being Element of I such that
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 H_{1}(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 H_{1}(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 H_{1}(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 H_{1}(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 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_{1}(i,j)
by A1;

hence q in union H_{1}(i,j)
by P1, TARSKI:def 4; :: thesis: verum

end;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

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 H

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 H

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 H

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

hence q in union H

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

then union H

then reconsider Y = union { (union H

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

defpred S
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 H_{1}(i,j)
by R1;

union H_{1}(i,j) in { (union H_{1}(i,j)) where i, j is Element of I : i <> j }
by A1;

hence q in Y by A2, TARSKI:def 4; :: thesis: verum

end;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 H

union H

hence q in Y by A2, TARSKI:def 4; :: thesis: verum

( $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

proof

consider f being Function of (XorDelta I),Y such that
let x be object ; :: thesis: ( x in XorDelta I implies ex y being object st

( y in Y & S_{1}[x,y] ) )

assume x in XorDelta I ; :: thesis: ex y being object st

( y in Y & S_{1}[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 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_{1}[x,y] )
by X0, P11, R2; :: thesis: verum

end;( y in Y & S

assume x in XorDelta I ; :: thesis: ex y being object st

( y in Y & S

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

P2: for x being object st x in XorDelta I holds

S

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 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: verum

end;( 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 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: verum