let f be FinSeq-Location ; :: thesis: for S being State of SCM holds not f in dom S
let S be State of SCM ; :: thesis: not f in dom S
A1: dom S = the carrier of SCM by PARTFUN1:def 4
.= SCM-Memory ;
f in SCM+FSA-Data*-Loc by Def5;
hence not f in dom S by A1, SCMFSA_1:33, XBOOLE_0:3; :: thesis: verum