scheme :: SCMPDS_4:sch 1
SCMPDSEx{ F1( set ) -> Integer, F2() -> Element of NAT } :
ex S being State of SCMPDS st
( IC S = F2() & ( for i being Nat holds S . (DataLoc (i,0)) = F1(i) ) )