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 = SCM-Memory by PARTFUN1:def 2;
f in SCM+FSA-Data*-Loc by Def5;
hence not f in dom S by A1, SCMFSA_1:30, XBOOLE_0:3; :: thesis: verum