:: deftheorem Def6 defines sumSCMFunction AMI_8:def 6 :
for b₁ being PartFunc of (FinPartSt SCM),(FinPartSt SCM) holds
( b₁ = sumSCMFunction iff for p, q being FinPartState of SCM holds
( [p,q] in b₁ iff ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0) & q = (dl. 2) .--> (Triangle n) ) ) );