let f be FinSeq-Location ; :: thesis: for s being State of SCM+FSA holds f in dom s
let s be State of SCM+FSA; :: thesis: f in dom s
dom s = SCM+FSA-Memory by PARTFUN1:def 2;
hence f in dom s ; :: thesis: verum