:: deftheorem defines SCM+FSA-Exec SCMFSA_1:def 17 :
for b₁ being Action of SCM+FSA-Instr,(product (SCM*-VAL * SCM+FSA-OK)) holds
( b₁ = SCM+FSA-Exec iff for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (b₁ . x) . y = SCM+FSA-Exec-Res (x,y) );