let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st I is_halting_on Initialized s,P holds
IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" ()),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))

let I be really-closed Program of SCM+FSA; :: thesis: for J being Program of SCM+FSA
for s being State of SCM+FSA st I is_halting_on Initialized s,P holds
IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" ()),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))

let J be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st I is_halting_on Initialized s,P holds
IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" ()),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))

let s be State of SCM+FSA; :: thesis: ( I is_halting_on Initialized s,P implies IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" ()),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) )
set s1 = Initialized s;
set P2 = P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ());
assume A1: I is_halting_on Initialized s,P ; :: thesis: IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" ()),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
Initialized s = Initialize () by MEMSTR_0:44;
then A2: P +* I halts_on Initialized s by ;
( P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ()) halts_on Initialized s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),()) = (LifeSpan ((P +* I),())) + 2 ) by ;
then A3: Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),()) = Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(),((LifeSpan ((P +* I),())) + 2)) by EXTPRO_1:23;
then DataPart (Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),())) = DataPart (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) by ;
then A4: DataPart (Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),())) = DataPart (Result ((P +* I),())) by
.= DataPart ((Result ((P +* I),())) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))) by MEMSTR_0:79 ;
IC (Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),())) = ((card I) + (card J)) + 1 by A1, A3, Lm6
.= IC ((Result ((P +* I),())) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))) by FUNCT_4:113 ;
then A5: Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),()) = (Result ((P +* I),())) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) by ;
A6: Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),()) = (Result ((P +* I),())) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) by A5;
thus IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" ()),P,s) = Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),()) by SCMFSA6B:def 1
.= (Result ((P +* I),())) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) by A6
.= (Result ((P +* I),())) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
.= (Result ((P +* I),())) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
.= (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) by SCMFSA6B:def 1 ; :: thesis: verum