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