let s be State of SCM+FSA; :: thesis: for i being Instruction of SCM holds (s | SCM-Memory) +* (NAT --> i) is State of SCM
let i be Instruction of SCM; :: thesis: (s | SCM-Memory) +* (NAT --> i) is State of SCM
reconsider s = s as SCM+FSA-State by PBOOLE:155;
(s | SCM-Memory) +* (NAT --> i) is State of SCM by SCMFSA_1:18;
hence (s | SCM-Memory) +* (NAT --> i) is State of SCM ; :: thesis: verum