let l be Element of NAT ; :: thesis: 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 ) )
let s be State of SCM+FSA; :: thesis: ( (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 ) )
consider La being Element of NAT such that
A1: l = La and
A2: goto l = SCM-goto La ;
reconsider S = s | SCM-Memory as State of SCM by Th73;
A3: Exec ((goto l),s) = s +* (Exec ((SCM-goto La),S)) by A2, Th75;
hence (Exec ((goto l),s)) . (IC ) = (Exec ((SCM-goto La),S)) . (IC ) by Th78
.= l by A1, AMI_3:7 ;
:: thesis: ( ( 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 ) )

hereby :: thesis: for f being FinSeq-Location holds (Exec ((goto l),s)) . f = s . f

let c be Int-Location ; :: thesis: (Exec ((goto l),s)) . c = s . c
reconsider C = c as Data-Location by Th25;
thus (Exec ((goto l),s)) . c = (Exec ((SCM-goto La),S)) . C by A3, Th79
.= S . C by AMI_3:7
.= s . c by Th80 ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (Exec ((goto l),s)) . f = s . f
A6: not f in dom (Exec ((SCM-goto La),S)) by Th68;
thus (Exec ((goto l),s)) . f = (s +* (Exec ((SCM-goto La),S))) . f by A3
.= s . f by A6, FUNCT_4:11 ; :: thesis: verum