let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for k being Integer holds
( (IExec ((a := k),s)) . a = k & ( for b being read-write Int-Location st b <> a holds
(IExec ((a := k),s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),s)) . f = s . f ) )
let a be read-write Int-Location ; :: thesis: for k being Integer holds
( (IExec ((a := k),s)) . a = k & ( for b being read-write Int-Location st b <> a holds
(IExec ((a := k),s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),s)) . f = s . f ) )
let k be Integer; :: thesis: ( (IExec ((a := k),s)) . a = k & ( for b being read-write Int-Location st b <> a holds
(IExec ((a := k),s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),s)) . f = s . f ) )
set s1 = s +* (Initialized (a := k));
A1: IExec ((a := k),s) = (Result ((ProgramPart (s +* (Initialized (a := k)))),(s +* (Initialized (a := k))))) +* (s | NAT) by SCMFSA6B:def 1;
intloc 0 in dom (Initialized (a := k)) by SCMFSA6A:45;
then A2: (s +* (Initialized (a := k))) . (intloc 0) = (Initialized (a := k)) . (intloc 0) by FUNCT_4:14
.= 1 by SCMFSA6A:46 ;
IC SCM+FSA in dom (Initialized (a := k)) by SCMFSA6A:24;
then (s +* (Initialized (a := k))) . (IC SCM+FSA) = (Initialized (a := k)) . (IC SCM+FSA) by FUNCT_4:14
.= 0 by SCMFSA6A:46 ;
then IC (s +* (Initialized (a := k))) = 0 ;
then reconsider s1 = s +* (Initialized (a := k)) as 0 -started State of SCM+FSA by COMPOS_1:def 20;
( Initialized (a := k) c= s1 & a := k c= Initialized (a := k) ) by FUNCT_4:26, SCMFSA6A:26;
then A4: a := k c= s1 by XBOOLE_1:1;
not a in NAT by SCMFSA_2:84;
then not a in (dom s) /\ NAT by XBOOLE_0:def 4;
then not a in dom (s | NAT) by RELAT_1:90;
hence (IExec ((a := k),s)) . a = (Result ((ProgramPart s1),s1)) . a by A1, FUNCT_4:12
.= k by A2, A4, SCMFSA_7:38 ;
:: thesis: ( ( for b being read-write Int-Location st b <> a holds
(IExec ((a := k),s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),s)) . f = s . f ) )

hereby :: thesis: for f being FinSeq-Location holds (IExec ((a := k),s)) . f = s . f

let b be read-write Int-Location ; :: thesis: ( b <> a implies (IExec ((a := k),s)) . b = s . b )
assume A6: b <> a ; :: thesis: (IExec ((a := k),s)) . b = s . b
A7: not b in dom (Initialized (a := k)) by SCMFSA6A:48;
not b in NAT by SCMFSA_2:84;
then not b in (dom s) /\ NAT by XBOOLE_0:def 4;
then not b in dom (s | NAT) by RELAT_1:90;
hence (IExec ((a := k),s)) . b = (Result ((ProgramPart s1),s1)) . b by A1, FUNCT_4:12
.= s1 . b by A2, A4, A6, SCMFSA_7:38
.= s . b by A7, FUNCT_4:12 ;
:: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (IExec ((a := k),s)) . f = s . f
A9: not f in dom (Initialized (a := k)) by SCMFSA6A:49;
not f in NAT by SCMFSA_2:85;
then not f in (dom s) /\ NAT by XBOOLE_0:def 4;
then not f in dom (s | NAT) by RELAT_1:90;
hence (IExec ((a := k),s)) . f = (Result ((ProgramPart s1),s1)) . f by A1, FUNCT_4:12
.= s1 . f by A2, A4, SCMFSA_7:38
.= s . f by A9, FUNCT_4:12 ;
:: thesis: verum