let s be State of SCM+FSA; :: thesis: for i being Instruction of SCM holds s | SCM-Memory is State of SCM
let i be Instruction of SCM; :: thesis: s | SCM-Memory is State of SCM
reconsider s = s as SCM+FSA-State by CARD_3:107;
s | SCM-Memory is SCM-State by SCMFSA_1:17;
then s | SCM-Memory is State of SCM by AMI_3:29;
hence s | SCM-Memory is State of SCM ; :: thesis: verum