let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for f being FinSeq-Location
for a being read-write Int-Location holds
( (IExec ((Stop SCM+FSA),p,s)) . a = s . a & (IExec ((Stop SCM+FSA),p,s)) . f = s . f )
let s be State of SCM+FSA; :: thesis: for f being FinSeq-Location
for a being read-write Int-Location holds
( (IExec ((Stop SCM+FSA),p,s)) . a = s . a & (IExec ((Stop SCM+FSA),p,s)) . f = s . f )
let f be FinSeq-Location ; :: thesis: for a being read-write Int-Location holds
( (IExec ((Stop SCM+FSA),p,s)) . a = s . a & (IExec ((Stop SCM+FSA),p,s)) . f = s . f )
let a be read-write Int-Location ; :: thesis: ( (IExec ((Stop SCM+FSA),p,s)) . a = s . a & (IExec ((Stop SCM+FSA),p,s)) . f = s . f )
A1: Initialized s = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:15;
A2: IExec ((Stop SCM+FSA),p,s) = Initialize (Initialized s) by SCMFSA8C:38
.= Initialize (Initialize (s +* ((intloc 0) .--> 1))) by SCMFSA6A:def 4, A1
.= (s +* ((intloc 0) .--> 1)) +* (Initialize (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= Initialized s by SCMFSA6A:def 4, A1 ;
hence (IExec ((Stop SCM+FSA),p,s)) . a = s . a by SCMFSA6C:3; :: thesis: (IExec ((Stop SCM+FSA),p,s)) . f = s . f
thus (IExec ((Stop SCM+FSA),p,s)) . f = s . f by A2, SCMFSA6C:3; :: thesis: verum