theorem Th3: :: SCMPDS_8:5

for a being Int_position ex f being Function of (product (the_Values_of SCMPDS)),NAT st
for s being State of SCMPDS holds
( ( s . a <= 0 implies f . s = 0 ) & ( s . a > 0 implies f . s = s . a ) )