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));
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
.= insloc 0 by SCMFSA6A:46 ;
then A1: IC (s +* (Initialized (a := k))) = insloc 0 by AMI_1:def 15;
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 ;
A3: Initialized (a := k) c= s +* (Initialized (a := k)) by FUNCT_4:26;
a := k c= Initialized (a := k) by SCMFSA6A:26;
then A4: a := k c= s +* (Initialized (a := k)) by A3, XBOOLE_1:1;
A5: IExec (a := k),s = (Result (s +* (Initialized (a := k)))) +* (s | NAT ) by SCMFSA6B:def 1;

now

assume A6: a in NAT ; :: thesis: contradiction
then reconsider a = a as Instruction-Location of SCM+FSA by AMI_1:def 4;
a in NAT by A6;
hence contradiction by SCMFSA_2:84; :: thesis: verum

end;

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 (s +* (Initialized (a := k)))) . a by A5, FUNCT_4:12
.= k by A1, 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 A7: b <> a ; :: thesis: (IExec (a := k),s) . b = s . b
A8: not b in dom (Initialized (a := k)) by SCMFSA6A:48;

now

assume A9: b in NAT ; :: thesis: contradiction
then reconsider b = b as Instruction-Location of SCM+FSA by AMI_1:def 4;
b in NAT by A9;
hence contradiction by SCMFSA_2:84; :: thesis: verum

end;

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 (s +* (Initialized (a := k)))) . b by A5, FUNCT_4:12
.= (s +* (Initialized (a := k))) . b by A1, A2, A4, A7, SCMFSA_7:38
.= s . b by A8, FUNCT_4:12 ;
:: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (IExec (a := k),s) . f = s . f
A10: not f in dom (Initialized (a := k)) by SCMFSA6A:49;

now

assume A11: f in NAT ; :: thesis: contradiction
then reconsider f = f as Instruction-Location of SCM+FSA by AMI_1:def 4;
f in NAT by A11;
hence contradiction by SCMFSA_2:85; :: thesis: verum

end;

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 (s +* (Initialized (a := k)))) . f by A5, FUNCT_4:12
.= (s +* (Initialized (a := k))) . f by A1, A2, A4, SCMFSA_7:38
.= s . f by A10, FUNCT_4:12 ;
:: thesis: verum