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 = the carrier of SCM+FSA by PARTFUN1:def 4
.= SCM+FSA-Memory ;
hence f in dom s ; :: thesis: verum