let p be PartState of SCM+FSA; :: thesis: ( p = x .--> i implies p is data-only )
assume Z: p = x .--> i ; :: thesis: p is data-only
A: dom p = {x} by Z, FUNCOP_1:13;
x <> IC by Th81;
then {x} misses {(IC )} by ZFMISC_1:11;
then dom p misses {(IC )} by A;
hence p is data-only by MEMSTR_0:def 6; :: thesis: verum