scheme :: SCMPDS_4:sch 1
SCMPDSEx{ F₁( set ) -> Integer, F₂() -> Element of NAT } :

ex S being State of SCMPDS st
( IC S = F₂() & ( for i being Nat holds S . (DataLoc (i,0)) = F₁(i) ) )