consider a, b, red, yellow, blue being set ;
set PLA = {0 };
set TRA = {a};
set CS = {red,yellow,blue};
set STA = [:{0 },{a}:];
[:{0 },{a}:] c= [:{0 },{a}:] ;
then reconsider STA = [:{0 },{a}:] as non empty Relation of {0 },{a} ;
set TSA = [:{a},{0 }:];
[:{a},{0 }:] c= [:{a},{0 }:] ;
then reconsider TSA = [:{a},{0 }:] as non empty Relation of {a},{0 } ;
consider fa being Function of (thin_cylinders {red,yellow,blue},{0 }),(thin_cylinders {red,yellow,blue},{0 });
set f = {a} --> fa;
take CPNT = Colored_PT_net_Str(# {0 },{a},STA,TSA,{red,yellow,blue},({a} --> fa) #); :: thesis: ( CPNT is strict & CPNT is Colored-PT-net-like )
A0: dom ({a} --> fa) = {a} by FUNCOP_1:19;

now

let x be set ; :: thesis: ( x in dom the firing-rule of CPNT implies x in the Transitions of CPNT \ (Outbds CPNT) )
assume A11: x in dom the firing-rule of CPNT ; :: thesis: x in the Transitions of CPNT \ (Outbds CPNT)
A13: x = a by A0, A11, TARSKI:def 1;
reconsider a1 = a as transition of CPNT by TARSKI:def 1;
( 0 in {0 } & a in {a} ) by TARSKI:def 1;
then [a1,0 ] in TSA by ZFMISC_1:106;
then aa: not {a1} *' = {} by PETRI:8;
not a1 in Outbds CPNT

proof

assume a1 in Outbds CPNT ; :: thesis: contradiction
then ex x being transition of CPNT st
( a1 = x & x is outbound ) ;
hence contradiction by aa, Def7; :: thesis: verum

end;

hence x in the Transitions of CPNT \ (Outbds CPNT) by A13, XBOOLE_0:def 5; :: thesis: verum

end;

then A1: dom the firing-rule of CPNT c= the Transitions of CPNT \ (Outbds CPNT) by TARSKI:def 3;

now

let t be transition of CPNT; :: thesis: ( t in dom the firing-rule of CPNT implies ex CS1 being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) st the firing-rule of CPNT . t is Function of (thin_cylinders CS1,I),(thin_cylinders CS1,O) )
assume t in dom the firing-rule of CPNT ; :: thesis: ex CS1 being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) st the firing-rule of CPNT . t is Function of (thin_cylinders CS1,I),(thin_cylinders CS1,O)
P1: t = a by TARSKI:def 1;
P2: ( 0 in {0 } & a in {a} ) by TARSKI:def 1;
then [a,0 ] in TSA by ZFMISC_1:106;
then pp: 0 in {t} *' by P1, PETRI:8;
[0 ,a] in STA by P2, ZFMISC_1:106;
then pa: 0 in *' {t} by P1, PETRI:6;
{red,yellow,blue} c= {red,yellow,blue} ;
then reconsider CS1 = {red,yellow,blue} as non empty Subset of the ColoredSet of CPNT ;
reconsider I = {0 } as Subset of (*' {t}) by pa, ZFMISC_1:37;
reconsider O = {0 } as Subset of ({t} *' ) by pp, ZFMISC_1:37;
P7: ({a} --> fa) . t = fa by FUNCOP_1:13;
fa is Function of (thin_cylinders CS1,I),(thin_cylinders CS1,O) ;
hence ex CS1 being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *' ) st the firing-rule of CPNT . t is Function of (thin_cylinders CS1,I),(thin_cylinders CS1,O) by P7; :: thesis: verum

end;

hence ( CPNT is strict & CPNT is Colored-PT-net-like ) by A1, Def4; :: thesis: verum