:: deftheorem defines constant VALUED_0:def 20 :
for s being ManySortedSet of NAT holds
( s is constant iff ex x being set st
for n being Nat holds s . n = x );