theorem Th37: :: AMI_8:37

for p being object holds
( p in dom sumSCMFunction iff ex n being Nat st p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0) )