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
f in SCM+FSA-Data*-Loc by Def3;
hence not f in dom S by SCMFSA_1:30, XBOOLE_0:3; :: thesis: verum