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 State of SCM by SCMFSA_1:17;
hence s | SCM-Memory is State of SCM ; :: thesis: verum