let f be FinSeq-Location ; :: thesis: for s being State of holds f in dom s
let s be State of ; :: thesis: f in dom s
dom s = dom SCM+FSA-OK by CARD_3:18
.= SCM+FSA-Memory by FUNCT_2:def 1 ;
hence f in dom s ; :: thesis: verum