let PTN be PT_net_Str ; :: thesis: for M0 being Boolean_marking of PTN
for t being transition of PTN
for s being place of PTN st s in {t} *' holds
(Firing t,M0) . s = TRUE
let M0 be Boolean_marking of PTN; :: thesis: for t being transition of PTN
for s being place of PTN st s in {t} *' holds
(Firing t,M0) . s = TRUE
let t be transition of PTN; :: thesis: for s being place of PTN st s in {t} *' holds
(Firing t,M0) . s = TRUE
let s be place of PTN; :: thesis: ( s in {t} *' implies (Firing t,M0) . s = TRUE )
assume A1: s in {t} *' ; :: thesis: (Firing t,M0) . s = TRUE
then A2: ((M0 +* ((*' {t}) --> FALSE )) +* (({t} *' ) --> TRUE )) .: ({t} *' ) = {TRUE } by Th5;
set M = (M0 +* ((*' {t}) --> FALSE )) +* (({t} *' ) --> TRUE );
A3: [#] the Places of PTN = the Places of PTN ;
A4: ( dom M0 = the Places of PTN & dom ((*' {t}) --> FALSE ) = *' {t} & dom (({t} *' ) --> TRUE ) = {t} *' ) by FUNCT_2:def 1;
then dom ((M0 +* ((*' {t}) --> FALSE )) +* (({t} *' ) --> TRUE )) = (dom (M0 +* ((*' {t}) --> FALSE ))) \/ ({t} *' ) by FUNCT_4:def 1
.= (the Places of PTN \/ (*' {t})) \/ ({t} *' ) by A4, FUNCT_4:def 1
.= the Places of PTN \/ ((*' {t}) \/ ({t} *' )) by XBOOLE_1:4
.= the Places of PTN by A3, SUBSET_1:28 ;
then ((M0 +* ((*' {t}) --> FALSE )) +* (({t} *' ) --> TRUE )) . s in {TRUE } by A1, A2, FUNCT_1:def 12;
hence (Firing t,M0) . s = TRUE by TARSKI:def 1; :: thesis: verum