let IT be PartState of SCM+FSA; :: thesis: ( IT = a .--> n implies IT is data-only )
assume Z: IT = a .--> n ; :: thesis: IT is data-only
B: dom IT = {a} by Z, FUNCOP_1:19;
A: dom IT misses {(IC )} by B, SCMFSA_2:81, ZFMISC_1:17;
a in Int-Locations by SCMFSA_2:9;
then C: dom IT c= Int-Locations by B, ZFMISC_1:37;
dom IT misses NAT by C, SCMFSA_2:13, XBOOLE_1:63;
hence dom IT misses {(IC )} \/ NAT by A, XBOOLE_1:70; :: according to COMPOS_1:def 23 :: thesis: verum