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