scheme :: SCMFSA_M:sch 1
SCMFSAEx{ F₁( set ) -> Integer, F₂( set ) -> FinSequence of INT , F₃() -> Element of NAT } :

ex S being State of SCM+FSA st
( IC S = F₃() & ( for i being Nat holds
( S . (intloc i) = F₁(i) & S . (fsloc i) = F₂(i) ) ) )