theorem :: SCMFSA8A:16

for P being preProgram of SCM+FSA
for x being set st x in dom P holds
( ( P . x = halt SCM+FSA implies (Directed P) . x = goto (card P) ) & ( P . x <> halt SCM+FSA implies (Directed P) . x = P . x ) ) by FUNCT_4:105, FUNCT_4:106;