theorem Th3: :: SCPINVAR:3

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) ) )