let g be FinSeq-Location ; :: thesis: for c being Int-Location
for s being State of SCM+FSA holds
( (Exec (c :=len g),s) . (IC SCM+FSA ) = Next & (Exec (c :=len g),s) . c = len (s . g) & ( for b being Int-Location st b <> c holds
(Exec (c :=len g),s) . b = s . b ) & ( for f being FinSeq-Location holds (Exec (c :=len g),s) . f = s . f ) )
let c be Int-Location ; :: thesis: for s being State of SCM+FSA holds
( (Exec (c :=len g),s) . (IC SCM+FSA ) = Next & (Exec (c :=len g),s) . c = len (s . g) & ( for b being Int-Location st b <> c holds
(Exec (c :=len g),s) . b = s . b ) & ( for f being FinSeq-Location holds (Exec (c :=len g),s) . f = s . f ) )
let s be State of SCM+FSA ; :: thesis: ( (Exec (c :=len g),s) . (IC SCM+FSA ) = Next & (Exec (c :=len g),s) . c = len (s . g) & ( for b being Int-Location st b <> c holds
(Exec (c :=len g),s) . b = s . b ) & ( for f being FinSeq-Location holds (Exec (c :=len g),s) . f = s . f ) )
reconsider ml = c as Element of SCM+FSA-Data-Loc by Def4;
reconsider p = g as Element of SCM+FSA-Data*-Loc by Def5;
reconsider I = c :=len g as Element of SCM+FSA-Instr ;
reconsider S = s as SCM+FSA-State ;
reconsider J = 11 as Element of Segm 13 by GR_CY_1:10;
A1: I = [J,<*ml,p*>] ;
A2: InsCode I = 11 by MCART_1:7;
A3: I `2 = <*ml,p*> by MCART_1:7;
set S1 = SCM+FSA-Chg S,(I int_addr3 ),(len (S . (I coll_addr2 )));
A4: Exec (c :=len g),s = SCM+FSA-Exec-Res I,S by SCMFSA_1:def 18
.= SCM+FSA-Chg (SCM+FSA-Chg S,(I int_addr3 ),(len (S . (I coll_addr2 )))),(succ (IC S)) by A2, SCMFSA_1:def 17 ;
A5: I int_addr3 = ml by A1, A3, SCMFSA_1:def 13;
thus (Exec (c :=len g),s) . (IC SCM+FSA ) = Next by A4, Th7, SCMFSA_1:20; :: thesis: ( (Exec (c :=len g),s) . c = len (s . g) & ( for b being Int-Location st b <> c holds
(Exec (c :=len g),s) . b = s . b ) & ( for f being FinSeq-Location holds (Exec (c :=len g),s) . f = s . f ) )
A6: I coll_addr2 = p by A1, A3, SCMFSA_1:def 14;
thus (Exec (c :=len g),s) . c = (SCM+FSA-Chg S,(I int_addr3 ),(len (S . (I coll_addr2 )))) . ml by A4, SCMFSA_1:21
.= len (s . g) by A5, A6, SCMFSA_1:25 ; :: thesis: ( ( for b being Int-Location st b <> c holds
(Exec (c :=len g),s) . b = s . b ) & ( for f being FinSeq-Location holds (Exec (c :=len g),s) . f = s . f ) )

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

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

end;

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