theorem Th2: :: SCPINVAR:2

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