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:11 ;
assume A4: s in {t} *' ; :: thesis: (Firing (t,M0)) . s = TRUE
then ((M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE)) .: ({t} *') = {TRUE} by Th4;
then ((M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE)) . s in {TRUE} by A4, A3, FUNCT_1:def 6;
hence (Firing (t,M0)) . s = TRUE by TARSKI:def 1; :: thesis: verum