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