set PLA = {0};
consider a, b, red, yellow, blue being set ;
set TRA = {a};
set TSA = [:{a},{0}:];
[:{a},{0}:] c= [:{a},{0}:] ;
then reconsider TSA = [:{a},{0}:] as non empty Relation of {a},{0} ;
set STA = [:{0},{a}:];
[:{0},{a}:] c= [:{0},{a}:] ;
then reconsider STA = [:{0},{a}:] as non empty Relation of {0},{a} ;
set CS = {red,yellow,blue};
consider fa being Function of (thin_cylinders ({red,yellow,blue},{0})),(thin_cylinders ({red,yellow,blue},{0}));
set f = {a} --> fa;
set CPNT = Colored_PT_net_Str(# {0},{a},STA,TSA,{red,yellow,blue},({a} --> fa) #);
A: Colored_PT_net_Str(# {0},{a},STA,TSA,{red,yellow,blue},({a} --> fa) #) is with_S-T_arc by PETRI:def 1;
Colored_PT_net_Str(# {0},{a},STA,TSA,{red,yellow,blue},({a} --> fa) #) is with_T-S_arc by PETRI:def 2;
then reconsider CPNT = Colored_PT_net_Str(# {0},{a},STA,TSA,{red,yellow,blue},({a} --> fa) #) as Colored_Petri_net by A;
take CPNT ; :: thesis:

{red,yellow,blue} c= {red,yellow,blue} ;
then reconsider CS1 = {red,yellow,blue} as non empty Subset of the ColoredSet of CPNT ;
let t be transition of CPNT; :: thesis:
assume t in dom the firing-rule of CPNT ; :: thesis:
A2: t = a by TARSKI:def 1;
A3: a in {a} by TARSKI:def 1;
A4: 0 in {0} by TARSKI:def 1;
then [a,0] in TSA by A3, ZFMISC_1:106;
then 0 in {t} *' by A2, PETRI:8;
then reconsider O = {0} as Subset of ({t} *') by ZFMISC_1:37;
[0,a] in STA by A4, A3, ZFMISC_1:106;
then 0 in *' {t} by A2, PETRI:6;
then reconsider I = {0} as Subset of (*' {t}) by ZFMISC_1:37;
A5: fa is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O)) ;
({a} --> fa) . t = fa by FUNCOP_1:13;
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 A5; :: thesis:

end;

end;

end;