deffunc H1( Element of I) -> set = the carrier of (CPNT . \$1);
consider P being ManySortedSet of I such that
AS1: for i being Element of I holds P . i = H1(i) from PBOOLE:sch 5();
deffunc H2( Element of I) -> set = the carrier' of (CPNT . \$1);
consider T being ManySortedSet of I such that
AS2: for i being Element of I holds T . i = H2(i) from PBOOLE:sch 5();
deffunc H3( Element of I) -> Element of bool [: the carrier of (CPNT . \$1), the carrier' of (CPNT . \$1):] = the S-T_Arcs of (CPNT . \$1);
consider ST being ManySortedSet of I such that
AS3: for i being Element of I holds ST . i = H3(i) from PBOOLE:sch 5();
deffunc H4( Element of I) -> Element of bool [: the carrier' of (CPNT . \$1), the carrier of (CPNT . \$1):] = the T-S_Arcs of (CPNT . \$1);
consider TS being ManySortedSet of I such that
AS4: for i being Element of I holds TS . i = H4(i) from PBOOLE:sch 5();
deffunc H5( Element of I) -> set = the ColoredSet of (CPNT . \$1);
consider CS being ManySortedSet of I such that
AS5: for i being Element of I holds CS . i = H5(i) from PBOOLE:sch 5();
deffunc H6( Element of I) -> set = the firing-rule of (CPNT . \$1);
consider F being ManySortedSet of I such that
AS6: for i being Element of I holds F . i = H6(i) from PBOOLE:sch 5();
deffunc H7( Element of I) -> set = dom the firing-rule of (CPNT . \$1);
consider DM being ManySortedSet of I such that
DM1: for i being Element of I holds DM . i = H7(i) from PBOOLE:sch 5();
deffunc H8( Element of I) -> set = rng the firing-rule of (CPNT . \$1);
consider RG being ManySortedSet of I such that
RG1: for i being Element of I holds RG . i = H8(i) from PBOOLE:sch 5();
set i = the Element of I;
P . the Element of I = the carrier of (CPNT . the Element of I) by AS1;
then consider x being object such that
S1: x in P . the Element of I by XBOOLE_0:def 1;
reconsider P0 = union (rng P) as non empty set by ;
set i = the Element of I;
T . the Element of I = the carrier' of (CPNT . the Element of I) by AS2;
then consider x being object such that
S2: x in T . the Element of I by XBOOLE_0:def 1;
reconsider T0 = union (rng T) as non empty set by ;
s: for X being set st X in rng ST holds
X c= [:P0,T0:]
proof
let X be set ; :: thesis: ( X in rng ST implies X c= [:P0,T0:] )
assume X in rng ST ; :: thesis: X c= [:P0,T0:]
then consider i being object such that
L1: ( i in dom ST & X = ST . i ) by FUNCT_1:def 3;
reconsider i = i as Element of I by L1;
l2: X = the S-T_Arcs of (CPNT . i) by ;
l3: ( the carrier' of (CPNT . i) = T . i & the carrier of (CPNT . i) = P . i ) by ;
L4: T . i c= T0 by ZFMISC_1:74;
P . i c= P0 by ZFMISC_1:74;
then [:(P . i),(T . i):] c= [:P0,T0:] by ;
hence X c= [:P0,T0:] by l3, l2; :: thesis: verum
end;
set i = the Element of I;
ST . the Element of I = the S-T_Arcs of (CPNT . the Element of I) by AS3;
then consider x being object such that
S1: x in ST . the Element of I by XBOOLE_0:def 1;
reconsider ST0 = union (rng ST) as non empty Relation of P0,T0 by ;
for X being set st X in rng TS holds
X c= [:T0,P0:]
proof
let X be set ; :: thesis: ( X in rng TS implies X c= [:T0,P0:] )
assume X in rng TS ; :: thesis: X c= [:T0,P0:]
then consider i being object such that
L1: ( i in dom TS & X = TS . i ) by FUNCT_1:def 3;
reconsider i = i as Element of I by L1;
l2: X = the T-S_Arcs of (CPNT . i) by ;
l3: ( the carrier' of (CPNT . i) = T . i & the carrier of (CPNT . i) = P . i ) by ;
L4: T . i c= T0 by ZFMISC_1:74;
P . i c= P0 by ZFMISC_1:74;
then [:(T . i),(P . i):] c= [:T0,P0:] by ;
hence X c= [:T0,P0:] by l3, l2; :: thesis: verum
end;
then PTS0: union (rng TS) c= [:T0,P0:] by ZFMISC_1:76;
for X being set st X in rng O holds
X c= [:T0,P0:]
proof
let X be set ; :: thesis: ( X in rng O implies X c= [:T0,P0:] )
assume X in rng O ; :: thesis: X c= [:T0,P0:]
then consider z being object such that
L1: ( z in dom O & X = O . z ) by FUNCT_1:def 3;
z in XorDelta I by L1;
then consider i, j being Element of I such that
L11: ( z = [i,j] & i <> j ) ;
l12: O . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) by ;
L14: ( the carrier' of (CPNT . i) = T . i & the carrier of (CPNT . j) = P . j ) by ;
L4: T . i c= T0 by ZFMISC_1:74;
P . j c= P0 by ZFMISC_1:74;
then L13: [:(T . i),(P . j):] c= [:T0,P0:] by ;
[:(Outbds (CPNT . i)), the carrier of (CPNT . j):] c= [:(T . i),(P . j):] by ;
hence X c= [:T0,P0:] by L13, l12, L11, L1; :: thesis: verum
end;
then t: union (rng O) c= [:T0,P0:] by ZFMISC_1:76;
set i = the Element of I;
TS . the Element of I = the T-S_Arcs of (CPNT . the Element of I) by AS4;
then consider x being object such that
S1: x in TS . the Element of I by XBOOLE_0:def 1;
x in union (rng TS) by ;
then reconsider TS0 = (union (rng TS)) \/ (union (rng O)) as non empty Relation of T0,P0 by ;
LL0: for X being set st X in rng CS holds
X is finite
proof
let X be set ; :: thesis: ( X in rng CS implies X is finite )
assume X in rng CS ; :: thesis: X is finite
then consider i being object such that
LL1: ( i in dom CS & X = CS . i ) by FUNCT_1:def 3;
reconsider i = i as Element of I by LL1;
X = the ColoredSet of (CPNT . i) by ;
hence X is finite ; :: thesis: verum
end;
ll3: dom CS is finite ;
set i = the Element of I;
CS . the Element of I = the ColoredSet of (CPNT . the Element of I) by AS5;
then consider x being object such that
S5: x in CS . the Element of I by XBOOLE_0:def 1;
reconsider CS0 = union (rng CS) as non empty finite set by ;
LL41: for i being object st i in I holds
ex f being Function st
( f = F . i & dom f = DM . i & rng f = RG . i )
proof
let i be object ; :: thesis: ( i in I implies ex f being Function st
( f = F . i & dom f = DM . i & rng f = RG . i ) )

assume i in I ; :: thesis: ex f being Function st
( f = F . i & dom f = DM . i & rng f = RG . i )

then reconsider i0 = i as Element of I ;
P04: F . i0 = the firing-rule of (CPNT . i0) by AS6;
then reconsider f = F . i as Function ;
take f ; :: thesis: ( f = F . i & dom f = DM . i & rng f = RG . i )
thus f = F . i ; :: thesis: ( dom f = DM . i & rng f = RG . i )
thus dom f = DM . i by ; :: thesis: rng f = RG . i
thus rng f = RG . i by ; :: thesis: verum
end;
for i, j being object
for f, g being Function st i in I & j in I & i <> j & f = F . i & g = F . j holds
dom f misses dom g
proof
let i0, j0 be object ; :: thesis: for f, g being Function st i0 in I & j0 in I & i0 <> j0 & f = F . i0 & g = F . j0 holds
dom f misses dom g

let f, g be Function; :: thesis: ( i0 in I & j0 in I & i0 <> j0 & f = F . i0 & g = F . j0 implies dom f misses dom g )
assume AA1: ( i0 in I & j0 in I & i0 <> j0 & f = F . i0 & g = F . j0 ) ; :: thesis:
then reconsider i = i0, j = j0 as Element of I ;
AA4: dom f = dom the firing-rule of (CPNT . i) by ;
AA5: dom g = dom the firing-rule of (CPNT . j) by ;
AA6: ( dom the firing-rule of (CPNT . i) c= the carrier' of (CPNT . i) \ (Outbds (CPNT . i)) & dom the firing-rule of (CPNT . j) c= the carrier' of (CPNT . j) \ (Outbds (CPNT . j)) ) by PETRI_2:def 11;
thus dom f misses dom g :: thesis: verum
proof
assume not dom f misses dom g ; :: thesis: contradiction
then (dom f) /\ (dom g) <> {} by XBOOLE_0:def 7;
then consider x being object such that
AA8: x in (dom f) /\ (dom g) by XBOOLE_0:def 1;
x in dom f by ;
then a9: x in the carrier' of (CPNT . i) \ (Outbds (CPNT . i)) by ;
x in dom g by ;
then x in the carrier' of (CPNT . j) \ (Outbds (CPNT . j)) by ;
then the carrier' of (CPNT . i) /\ the carrier' of (CPNT . j) <> {} by ;
hence contradiction by AS, AA1, XBOOLE_0:def 7; :: thesis: verum
end;
end;
then consider F0 being Function such that
LL43: ( F0 = union (rng F) & dom F0 = union (rng DM) & rng F0 = union (rng RG) & ( for i, x being object
for f being Function st i in I & f = F . i & x in dom f holds
F0 . x = f . x ) ) by ;
reconsider UQ = union (rng q) as Function by ;
set UF0 = F0 +* UQ;
reconsider SCPNT = Colored_PT_net_Str(# P0,T0,ST0,TS0,CS0,(F0 +* UQ) #) as strict Colored_Petri_net by ;
deffunc H9( Element of I) -> Element of bool the carrier' of (CPNT . \$1) = Outbds (CPNT . \$1);
consider OU being Function such that
OU1: ( dom OU = I & ( for i being Element of I holds OU . i = H9(i) ) ) from reconsider OU = OU as I -defined Function by ;
reconsider OU = OU as ManySortedSet of I by ;
for x0 being object st x0 in Outbds SCPNT holds
x0 in union (rng OU)
proof
let x0 be object ; :: thesis: ( x0 in Outbds SCPNT implies x0 in union (rng OU) )
assume x0 in Outbds SCPNT ; :: thesis: x0 in union (rng OU)
then consider x1 being transition of SCPNT such that
OU2: ( x0 = x1 & x1 is outbound ) ;
consider Z being set such that
OU3: ( x1 in Z & Z in rng T ) by TARSKI:def 4;
consider i being object such that
OU4: ( i in dom T & Z = T . i ) by ;
reconsider i = i as Element of I by OU4;
reconsider xi = x1 as transitions of (CPNT . i) by ;
{xi} *' = {}
proof
assume {xi} *' <> {} ; :: thesis: contradiction
then consider z being object such that
OU61: z in {xi} *' by XBOOLE_0:def 1;
consider si being place of (CPNT . i) such that
OU62: ( z = si & ex fi being T-S_arc of (CPNT . i) ex ti being transition of (CPNT . i) st
( ti in {xi} & fi = [ti,si] ) ) by OU61;
consider fi being T-S_arc of (CPNT . i), ti being transition of (CPNT . i) such that
OU63: ( ti in {xi} & fi = [ti,si] ) by OU62;
SS0: P . i = the carrier of (CPNT . i) by AS1;
reconsider ss = si as place of SCPNT by ;
TS0: TS . i = the T-S_Arcs of (CPNT . i) by AS4;
fi in union (rng TS) by ;
then reconsider ff = fi as T-S_arc of SCPNT by XBOOLE_0:def 3;
TT0: T . i = the carrier' of (CPNT . i) by AS2;
reconsider tt = ti as transition of SCPNT by ;
ff = [tt,ss] by OU63;
then ss in { s where s is place of SCPNT : ex f being T-S_arc of SCPNT ex t being transition of SCPNT st
( t in {x1} & f = [t,s] )
}
by OU63;
hence contradiction by OU2; :: thesis: verum
end;
then xi is outbound ;
then OU6: xi in Outbds (CPNT . i) ;
OU . i = Outbds (CPNT . i) by OU1;
hence x0 in union (rng OU) by ; :: thesis: verum
end;
then OU2: Outbds SCPNT c= union (rng OU) ;
XX3: for i, j being object st i in I & j in I & i <> j holds
(T . i) /\ (OU . j) = {}
proof
let i0, j0 be object ; :: thesis: ( i0 in I & j0 in I & i0 <> j0 implies (T . i0) /\ (OU . j0) = {} )
assume XXX: ( i0 in I & j0 in I & i0 <> j0 ) ; :: thesis: (T . i0) /\ (OU . j0) = {}
then reconsider i = i0, j = j0 as Element of I ;
P1: the carrier' of (CPNT . i) /\ (Outbds (CPNT . j)) c= the carrier' of (CPNT . i) /\ the carrier' of (CPNT . j) by XBOOLE_1:26;
p2: the carrier' of (CPNT . i) /\ (Outbds (CPNT . j)) c= {} by ;
the carrier' of (CPNT . i) = T . i by AS2;
hence (T . i0) /\ (OU . j0) = {} by ; :: thesis: verum
end;
v: for i being object st i in I holds
DM . i c= (T (\) OU) . i
proof
let i0 be object ; :: thesis: ( i0 in I implies DM . i0 c= (T (\) OU) . i0 )
assume i0 in I ; :: thesis: DM . i0 c= (T (\) OU) . i0
then reconsider i = i0 as Element of I ;
P1: DM . i = dom the firing-rule of (CPNT . i) by DM1;
P2: dom the firing-rule of (CPNT . i) c= the carrier' of (CPNT . i) \ (Outbds (CPNT . i)) by PETRI_2:def 11;
P3: the carrier' of (CPNT . i) = T . i by AS2;
(T (\) OU) . i = (T . i) \ (OU . i) by PBOOLE:def 6;
hence DM . i0 c= (T (\) OU) . i0 by P1, P2, P3, OU1; :: thesis: verum
end;
XXX2: ( union (rng DM) = Union DM & union (rng T) = Union T & union (rng OU) = Union OU ) by CARD_3:def 4;
then XXX3A: dom F0 c= the carrier' of SCPNT \ (Union OU) by ;
xx: the carrier' of SCPNT \ (union (rng OU)) c= the carrier' of SCPNT \ (Outbds SCPNT) by ;
for x being object st x in dom the firing-rule of SCPNT holds
x in the carrier' of SCPNT \ (Outbds SCPNT)
proof
let x be object ; :: thesis: ( x in dom the firing-rule of SCPNT implies x in the carrier' of SCPNT \ (Outbds SCPNT) )
assume x in dom the firing-rule of SCPNT ; :: thesis: x in the carrier' of SCPNT \ (Outbds SCPNT)
per cases then ( x in dom F0 or x in dom UQ ) by FUNCT_4:12;
suppose x in dom F0 ; :: thesis: x in the carrier' of SCPNT \ (Outbds SCPNT)
hence x in the carrier' of SCPNT \ (Outbds SCPNT) by ; :: thesis: verum
end;
suppose AG1: x in dom UQ ; :: thesis: x in the carrier' of SCPNT \ (Outbds SCPNT)
consider s being object such that
D2: [x,s] in UQ by ;
consider i, j being Element of I, q12 being Function, O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) such that
D3: ( i <> 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)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & [x,s] in q12 ) by LMQ1, AS, D2;
CT1: ( the carrier' of (CPNT . i) = T . i & the carrier of (CPNT . j) = P . j ) by ;
x in dom q12 by ;
then S0: x in Outbds (CPNT . i) by ;
w: T . i c= T0 by ZFMISC_1:74;
then S2: x in the carrier' of SCPNT by ;
reconsider t = x as transition of SCPNT by w, S0, CT1;
t in dom O12 by ;
then consider s being object such that
A65: [t,s] in O12 by XTUPLE_0:def 12;
[i,j] in XorDelta I by D3;
then [i,j] in dom O by PARTFUN1:def 2;
then O . [i,j] in rng O by FUNCT_1:3;
then [t,s] in union (rng O) by ;
then reconsider f = [t,s] as T-S_arc of SCPNT by XBOOLE_0:def 3;
A68: f = [t,s] ;
A69: t in {t} by TARSKI:def 1;
U2: s in the carrier of (CPNT . j) by ;
P . j c= P0 by ZFMISC_1:74;
then s in {t} *' by A69, A68, U2, CT1;
then for w being transition of SCPNT holds
( not t = w or not w is outbound ) ;
then not x in Outbds SCPNT ;
hence x in the carrier' of SCPNT \ (Outbds SCPNT) by ; :: thesis: verum
end;
end;
end;
then CP1: dom the firing-rule of SCPNT c= the carrier' of SCPNT \ (Outbds SCPNT) ;
for t being transition of SCPNT st t in dom the firing-rule of SCPNT holds
ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))
proof
let t be transition of SCPNT; :: thesis: ( t in dom the firing-rule of SCPNT implies ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) )
assume d: t in dom the firing-rule of SCPNT ; :: thesis: ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))
per cases ( not t in dom UQ or t in dom UQ ) ;
suppose AG01: not t in dom UQ ; :: thesis: ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))
then AG0: t in dom F0 by ;
consider Z being set such that
XOU3: ( t in Z & Z in rng T ) by TARSKI:def 4;
consider i being object such that
XOU4: ( i in dom T & Z = T . i ) by ;
reconsider i = i as Element of I by XOU4;
reconsider ti = t as transitions of (CPNT . i) by ;
consider Z being set such that
POU3: ( t in Z & Z in rng DM ) by ;
consider j being object such that
POU4: ( j in dom DM & Z = DM . j ) by ;
reconsider j = j as Element of I by POU4;
OU6: DM . j = dom the firing-rule of (CPNT . j) by DM1;
i = j
proof
assume OU71: i <> j ; :: thesis: contradiction
OU72: t in the carrier' of (CPNT . i) by ;
dom the firing-rule of (CPNT . j) c= the carrier' of (CPNT . j) \ (Outbds (CPNT . j)) by PETRI_2:def 11;
then t in the carrier' of (CPNT . j) \ (Outbds (CPNT . j)) by ;
then the carrier' of (CPNT . i) /\ the carrier' of (CPNT . j) <> {} by ;
hence contradiction by AS, OU71, XBOOLE_0:def 7; :: thesis: verum
end;
then OU8: ti in dom the firing-rule of (CPNT . i) by ;
consider CSi being non empty Subset of the ColoredSet of (CPNT . i), Ii being Subset of (*' {ti}), Oi being Subset of ({ti} *') such that
OU9: the firing-rule of (CPNT . i) . ti is Function of (thin_cylinders (CSi,Ii)),(thin_cylinders (CSi,Oi)) by ;
CC1: CS . i c= union (rng CS) by ZFMISC_1:74;
CS . i = the ColoredSet of (CPNT . i) by AS5;
then reconsider CS = CSi as non empty Subset of the ColoredSet of SCPNT by ;
Ii c= *' {t}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ii or x in *' {t} )
assume x in Ii ; :: thesis: x in *' {t}
then x in *' {ti} ;
then consider ssi being place of (CPNT . i) such that
XX1: ( x = ssi & ex ffi being S-T_arc of (CPNT . i) ex tti being transition of (CPNT . i) st
( tti in {ti} & ffi = [ssi,tti] ) ) ;
consider ffi being S-T_arc of (CPNT . i), tti being transition of (CPNT . i) such that
XX2: ( tti in {ti} & ffi = [ssi,tti] ) by XX1;
SS0: P . i = the carrier of (CPNT . i) by AS1;
reconsider ss = ssi as place of SCPNT by ;
ST0: ST . i = the S-T_Arcs of (CPNT . i) by AS3;
reconsider ff = ffi as S-T_arc of SCPNT by ;
tti = t by ;
then reconsider tt = tti as transition of SCPNT ;
ff = [ss,tt] by XX2;
hence x in *' {t} by ; :: thesis: verum
end;
then reconsider I0 = Ii as Subset of (*' {t}) ;
Oi c= {t} *'
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Oi or x in {t} *' )
assume x in Oi ; :: thesis: x in {t} *'
then x in {ti} *' ;
then consider ssi being place of (CPNT . i) such that
XX1: ( x = ssi & ex ffi being T-S_arc of (CPNT . i) ex tti being transition of (CPNT . i) st
( tti in {ti} & ffi = [tti,ssi] ) ) ;
consider ffi being T-S_arc of (CPNT . i), tti being transition of (CPNT . i) such that
XX2: ( tti in {ti} & ffi = [tti,ssi] ) by XX1;
SS0: P . i = the carrier of (CPNT . i) by AS1;
reconsider ss = ssi as place of SCPNT by ;
TS0: TS . i = the T-S_Arcs of (CPNT . i) by AS4;
ffi in union (rng TS) by ;
then reconsider ff = ffi as T-S_arc of SCPNT by XBOOLE_0:def 3;
tti = t by ;
then reconsider tt = tti as transition of SCPNT ;
ff = [tt,ss] by XX2;
hence x in {t} *' by ; :: thesis: verum
end;
then reconsider O = Oi as Subset of ({t} *') ;
Y1: F . i = the firing-rule of (CPNT . i) by AS6;
the firing-rule of SCPNT . t = F0 . t by
.= the firing-rule of (CPNT . i) . ti by ;
then the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I0)),(thin_cylinders (CS,O)) by OU9;
hence ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ; :: thesis: verum
end;
suppose AG1: t in dom UQ ; :: thesis: ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O))
then consider s being object such that
D2: [t,s] in UQ by XTUPLE_0:def 12;
consider i, j being Element of I, q12 being Function, O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) such that
D3: ( i <> 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)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & [t,s] in q12 ) by LMQ1, AS, D2;
CT1: the ColoredSet of (CPNT . i) = CS . i by AS5;
DF1: t in dom q12 by ;
then S0: t in Outbds (CPNT . i) by ;
then reconsider ti = t as transition of (CPNT . i) ;
v8: ex x being transition of (CPNT . i) st
( ti = x & x is outbound ) by S0;
CS . i = the ColoredSet of (CPNT . i) by AS5;
then reconsider CS0 = CS . i as non empty Subset of the ColoredSet of SCPNT by ZFMISC_1:74;
*' {ti} c= *' {t}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in *' {ti} or x in *' {t} )
assume x in *' {ti} ; :: thesis: x in *' {t}
then consider ssi being place of (CPNT . i) such that
XX1: ( x = ssi & ex ffi being S-T_arc of (CPNT . i) ex tti being transition of (CPNT . i) st
( tti in {ti} & ffi = [ssi,tti] ) ) ;
consider ffi being S-T_arc of (CPNT . i), tti being transition of (CPNT . i) such that
XX2: ( tti in {ti} & ffi = [ssi,tti] ) by XX1;
SS0: P . i = the carrier of (CPNT . i) by AS1;
reconsider ss = ssi as place of SCPNT by ;
ST0: ST . i = the S-T_Arcs of (CPNT . i) by AS3;
reconsider ff = ffi as S-T_arc of SCPNT by ;
tti = t by ;
then reconsider tt = tti as transition of SCPNT ;
ff = [ss,tt] by XX2;
hence x in *' {t} by ; :: thesis: verum
end;
then reconsider I0 = *' {ti} as Subset of (*' {t}) ;
Im (O12,ti) c= {t} *'
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Im (O12,ti) or x in {t} *' )
assume A41: x in Im (O12,ti) ; :: thesis: x in {t} *'
then reconsider sj = x as place of (CPNT . j) ;
A42: [ti,sj] in O12 by ;
[i,j] in XorDelta I by D3;
then [i,j] in dom O by PARTFUN1:def 2;
then O . [i,j] in rng O by FUNCT_1:3;
then [ti,sj] in union (rng O) by ;
then reconsider f = [t,sj] as T-S_arc of SCPNT by XBOOLE_0:def 3;
CT1: the carrier of (CPNT . j) = P . j by AS1;
P . j c= P0 by ZFMISC_1:74;
then reconsider s = sj as place of SCPNT by CT1;
A44: f = [t,s] ;
t in {t} by TARSKI:def 1;
hence x in {t} *' by A44; :: thesis: verum
end;
then reconsider O0 = Im (O12,ti) as Subset of ({t} *') ;
the firing-rule of SCPNT . t = UQ . t by
.= q12 . ti by ;
then the firing-rule of SCPNT . t is Function of (thin_cylinders (CS0,I0)),(thin_cylinders (CS0,O0)) by v8, CT1, D3;
hence ex CS being non empty Subset of the ColoredSet of SCPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of SCPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ; :: thesis: verum
end;
end;
end;
then reconsider SCPNT = Colored_PT_net_Str(# P0,T0,ST0,TS0,CS0,(F0 +* UQ) #) as strict Colored-PT-net by ;
take SCPNT ; :: thesis: ex P, T, ST, TS, CS, F being ManySortedSet of I ex UF, UQ being Function st
( ( for i being Element of I holds
( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) & F . i = the firing-rule of (CPNT . i) ) ) & UF = union (rng F) & UQ = union (rng q) & the carrier of SCPNT = union (rng P) & the carrier' of SCPNT = union (rng T) & the S-T_Arcs of SCPNT = union (rng ST) & the T-S_Arcs of SCPNT = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of SCPNT = union (rng CS) & the firing-rule of SCPNT = UF +* UQ )

thus ex P, T, ST, TS, CS, F being ManySortedSet of I ex UF, UQ being Function st
( ( for i being Element of I holds
( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) & F . i = the firing-rule of (CPNT . i) ) ) & UF = union (rng F) & UQ = union (rng q) & the carrier of SCPNT = union (rng P) & the carrier' of SCPNT = union (rng T) & the S-T_Arcs of SCPNT = union (rng ST) & the T-S_Arcs of SCPNT = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of SCPNT = union (rng CS) & the firing-rule of SCPNT = UF +* UQ ) by AS1, AS2, AS3, AS4, AS5, AS6, LL43; :: thesis: verum