let s be State of SCM+FSA ; :: thesis: for f being FinSeq-Location
for p being FinSequence of INT holds
( (IExec (f := p),s) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec (f := p),s) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec (f := p),s) . g = s . g ) )
let f be FinSeq-Location ; :: thesis: for p being FinSequence of INT holds
( (IExec (f := p),s) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec (f := p),s) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec (f := p),s) . g = s . g ) )
let p be FinSequence of INT ; :: thesis: ( (IExec (f := p),s) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec (f := p),s) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec (f := p),s) . g = s . g ) )
A1: IExec (f := p),s = (Result (ProgramPart (s +* (Initialized (f := p)))),(s +* (Initialized (f := p)))) +* (s | NAT ) by SCMFSA6B:def 1;
intloc 0 in dom (Initialized (f := p)) by SCMFSA6A:45;
then A2: (s +* (Initialized (f := p))) . (intloc 0 ) = (Initialized (f := p)) . (intloc 0 ) by FUNCT_4:14
.= 1 by SCMFSA6A:46 ;
IC SCM+FSA in dom (Initialized (f := p)) by SCMFSA6A:24;
then (s +* (Initialized (f := p))) . (IC SCM+FSA ) = (Initialized (f := p)) . (IC SCM+FSA ) by FUNCT_4:14
.= 0 by SCMFSA6A:46 ;
then A3: IC (s +* (Initialized (f := p))) = 0 by COMPOS_1:def 9;
( Initialized (f := p) c= s +* (Initialized (f := p)) & f := p c= Initialized (f := p) ) by FUNCT_4:26, SCMFSA6A:26;
then A4: f := p c= s +* (Initialized (f := p)) by XBOOLE_1:1;
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 (f := p),s) . f = (Result (ProgramPart (s +* (Initialized (f := p)))),(s +* (Initialized (f := p)))) . f by A1, FUNCT_4:12
.= p by A3, A2, A4, Lm4 ;
:: thesis: ( ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec (f := p),s) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec (f := p),s) . g = s . g ) )

hereby :: thesis: for g being FinSeq-Location st g <> f holds
(IExec (f := p),s) . g = s . g

let a be read-write Int-Location ; :: thesis: ( a <> intloc 1 & a <> intloc 2 implies (IExec (f := p),s) . a = s . a )
assume A6: ( a <> intloc 1 & a <> intloc 2 ) ; :: thesis: (IExec (f := p),s) . a = s . a
A7: not a in dom (Initialized (f := p)) by SCMFSA6A:48;
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 (f := p),s) . a = (Result (ProgramPart (s +* (Initialized (f := p)))),(s +* (Initialized (f := p)))) . a by A1, FUNCT_4:12
.= (s +* (Initialized (f := p))) . a by A3, A2, A4, A6, Lm4
.= s . a by A7, FUNCT_4:12 ;
:: thesis: verum

end;

let g be FinSeq-Location ; :: thesis: ( g <> f implies (IExec (f := p),s) . g = s . g )
assume A9: g <> f ; :: thesis: (IExec (f := p),s) . g = s . g
A10: not g in dom (Initialized (f := p)) by SCMFSA6A:49;
not g in NAT by SCMFSA_2:85;
then not g in (dom s) /\ NAT by XBOOLE_0:def 4;
then not g in dom (s | NAT ) by RELAT_1:90;
hence (IExec (f := p),s) . g = (Result (ProgramPart (s +* (Initialized (f := p)))),(s +* (Initialized (f := p)))) . g by A1, FUNCT_4:12
.= (s +* (Initialized (f := p))) . g by A3, A2, A4, A9, Lm4
.= s . g by A10, FUNCT_4:12 ;
:: thesis: verum