let PTN be Petri_net; :: 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 )
set M = (M0 +* ((*' {t}) --> FALSE )) +* (({t} *' ) --> TRUE );
A1: [#] the carrier of PTN = the carrier of PTN ;
A2: ( dom M0 = the carrier of PTN & dom ((*' {t}) --> FALSE ) = *' {t} ) by FUNCT_2:def 1;
dom (({t} *' ) --> TRUE ) = {t} *' by FUNCT_2:def 1;
then A3: dom ((M0 +* ((*' {t}) --> FALSE )) +* (({t} *' ) --> TRUE )) = (dom (M0 +* ((*' {t}) --> FALSE ))) \/ ({t} *' ) by FUNCT_4:def 1
.= (the carrier of PTN \/ (*' {t})) \/ ({t} *' ) by A2, FUNCT_4:def 1
.= the carrier of PTN \/ ((*' {t}) \/ ({t} *' )) by XBOOLE_1:4
.= the carrier of PTN by A1, SUBSET_1:28 ;
assume A4: s in {t} *' ; :: thesis: (Firing t,M0) . s = TRUE
then ((M0 +* ((*' {t}) --> FALSE )) +* (({t} *' ) --> TRUE )) .: ({t} *' ) = {TRUE } by Th5;
then ((M0 +* ((*' {t}) --> FALSE )) +* (({t} *' ) --> TRUE )) . s in {TRUE } by A4, A3, FUNCT_1:def 12;
hence (Firing t,M0) . s = TRUE by TARSKI:def 1; :: thesis: verum