let f be FinSeq-Location ; :: thesis: for a being Int-Location
for s being State of SCM+FSA holds {a,(IC ),f} c= dom s
let a be Int-Location; :: thesis: for s being State of SCM+FSA holds {a,(IC ),f} c= dom s
let s be State of SCM+FSA; :: thesis: {a,(IC ),f} c= dom s
A1: a in dom s by SCMFSA_2:42;
IC in dom s by MEMSTR_0:2;
then A2: {a,(IC )} c= dom s by A1, ZFMISC_1:32;
f in dom s by SCMFSA_2:43;
then {f} c= dom s by ZFMISC_1:31;
then {a,(IC )} \/ {f} c= dom s by A2, XBOOLE_1:8;
hence {a,(IC ),f} c= dom s by ENUMSET1:3; :: thesis: verum