:: deftheorem Def5 defines powerSCMFunction AMI_8:def 5 :
for b₁ being PartFunc of (FinPartSt SCM),(FinPartSt SCM) holds
( b₁ = powerSCMFunction 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,1) & q = (dl. 2) .--> (n !) ) ) );