let g be FinSeq-Location ; :: thesis: for c, a being Int-Location
for s being State of SCM+FSA holds
( (Exec (c := g,a),s) . (IC SCM+FSA ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . a) & (Exec (c := g,a),s) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds
(Exec (c := g,a),s) . b = s . b ) & ( for f being FinSeq-Location holds (Exec (c := g,a),s) . f = s . f ) )
let c, a be Int-Location ; :: thesis: for s being State of SCM+FSA holds
( (Exec (c := g,a),s) . (IC SCM+FSA ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . a) & (Exec (c := g,a),s) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds
(Exec (c := g,a),s) . b = s . b ) & ( for f being FinSeq-Location holds (Exec (c := g,a),s) . f = s . f ) )
let s be State of SCM+FSA ; :: thesis: ( (Exec (c := g,a),s) . (IC SCM+FSA ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . a) & (Exec (c := g,a),s) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds
(Exec (c := g,a),s) . b = s . b ) & ( for f being FinSeq-Location holds (Exec (c := g,a),s) . f = s . f ) )
reconsider p = g as Element of SCM+FSA-Data*-Loc by Def5;
reconsider mk = a, ml = c as Element of SCM+FSA-Data-Loc by Def4;
reconsider I = c := g,a as Element of SCM+FSA-Instr ;
reconsider S = s as SCM+FSA-State by PBOOLE:155;
reconsider J = 9 as Element of Segm 13 by NAT_1:45;
InsCode I = 9 by RECDEF_2:def 1;
then consider i being Integer, k being Element of NAT such that
A1: k = abs (S . (I int_addr2 )) and
A2: i = (S . (I coll_addr1 )) /. k and
A3: SCM+FSA-Exec-Res I,S = SCM+FSA-Chg (SCM+FSA-Chg S,(I int_addr1 ),i),(succ (IC S)) by SCMFSA_1:def 17;
set S1 = SCM+FSA-Chg S,(I int_addr1 ),i;
A4: Exec (c := g,a),s = SCM+FSA-Chg (SCM+FSA-Chg S,(I int_addr1 ),i),(succ (IC S)) by A3, SCMFSA_1:def 18;
hence (Exec (c := g,a),s) . (IC SCM+FSA ) = succ (IC s) by Th7, SCMFSA_1:20; :: thesis: ( ex k being Element of NAT st
( k = abs (s . a) & (Exec (c := g,a),s) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds
(Exec (c := g,a),s) . b = s . b ) & ( for f being FinSeq-Location holds (Exec (c := g,a),s) . f = s . f ) )
A5: ( I = [J,{} ,<*ml,p,mk*>] & I `3_3 = <*ml,p,mk*> ) by RECDEF_2:def 3;
then A6: I int_addr1 = ml by SCMFSA_1:def 10;
A7: I coll_addr1 = p by A5, SCMFSA_1:def 12;

hereby :: thesis: ( ( for b being Int-Location st b <> c holds
(Exec (c := g,a),s) . b = s . b ) & ( for f being FinSeq-Location holds (Exec (c := g,a),s) . f = s . f ) )

take k = k; :: thesis: ( k = abs (s . a) & (Exec (c := g,a),s) . c = (s . g) /. k )
thus k = abs (s . a) by A5, A1, SCMFSA_1:def 11; :: thesis: (Exec (c := g,a),s) . c = (s . g) /. k
thus (Exec (c := g,a),s) . c = (SCM+FSA-Chg S,(I int_addr1 ),i) . ml by A4, SCMFSA_1:21
.= (s . g) /. k by A2, A6, A7, SCMFSA_1:25 ; :: thesis: verum

end;

hereby :: thesis: for f being FinSeq-Location holds (Exec (c := g,a),s) . f = s . f

let b be Int-Location ; :: thesis: ( b <> c implies (Exec (c := g,a),s) . b = s . b )
reconsider mn = b as Element of SCM+FSA-Data-Loc by Def4;
assume A8: b <> c ; :: thesis: (Exec (c := g,a),s) . b = s . b
thus (Exec (c := g,a),s) . b = (SCM+FSA-Chg S,(I int_addr1 ),i) . mn by A4, SCMFSA_1:21
.= s . b by A6, A8, SCMFSA_1:26 ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (Exec (c := g,a),s) . f = s . f
reconsider q = f as Element of SCM+FSA-Data*-Loc by Def5;
thus (Exec (c := g,a),s) . f = (SCM+FSA-Chg S,(I int_addr1 ),i) . q by A4, SCMFSA_1:22
.= s . f by SCMFSA_1:27 ; :: thesis: verum