let f be FinSeq-Location ; :: thesis: for a being Int-Location
for s being State of SCM+FSA holds {a,(IC SCM+FSA ),f} c= dom s
let a be Int-Location ; :: thesis: for s being State of SCM+FSA holds {a,(IC SCM+FSA ),f} c= dom s
let s be State of SCM+FSA ; :: thesis: {a,(IC SCM+FSA ),f} c= dom s
A1: a in dom s by SCMFSA_2:66;
IC SCM+FSA in dom s by SCMFSA8B:1;
then A2: {a,(IC SCM+FSA )} c= dom s by A1, ZFMISC_1:38;
f in dom s by SCMFSA_2:67;
then {f} c= dom s by ZFMISC_1:37;
then {a,(IC SCM+FSA )} \/ {f} c= dom s by A2, XBOOLE_1:8;
hence {a,(IC SCM+FSA ),f} c= dom s by ENUMSET1:43; :: thesis: verum