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