theorem Th62: :: SCMFSA_2:69

for l being Nat
for s being State of SCM+FSA holds
( (Exec ((goto l),s)) . (IC ) = l & ( for c being Int-Location holds (Exec ((goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((goto l),s)) . f = s . f ) )