theorem Th57: :: SCMPDS_2:61

for k being Integer ex s being State of SCMPDS st
for d being Int_position holds s . d = k