let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def 4 :: thesis: for P being Instruction-Sequence of SCM+FSA st I ";" J c= P holds
for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( I ";" J c= P implies for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) )
assume A1: I ";" J c= P ; :: thesis: for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A2: I c= P +* I by FUNCT_4:25;
A3: P = P +* (I ";" J) by A1, FUNCT_4:98;

per cases ( P +* I halts_on s or not P +* I halts_on s ) ;

suppose A4: P +* I halts_on s ; :: thesis: for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

let k be Nat; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

hereby :: thesis: verum

per cases ( k <= LifeSpan ((P +* I),s) or k > LifeSpan ((P +* I),s) ) ;

suppose A5: k <= LifeSpan ((P +* I),s) ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

(Comput ((P +* I),s,k)) . (intloc 0) = s . (intloc 0) by Def2, A2;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A3, Th14, A4, A5; :: thesis: verum

end;

suppose A6: k > LifeSpan ((P +* I),s) ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

set LS = LifeSpan ((P +* I),s);
consider p being Element of NAT such that
A7: k = (LifeSpan ((P +* I),s)) + p and
A8: 1 <= p by A6, FINSEQ_4:84;
consider r being Nat such that
A9: p = 1 + r by A8, NAT_1:10;
( dom (Start-At (0,SCM+FSA)) = {(IC )} & intloc 0 <> IC ) by SCMFSA_2:56;
then A10: not intloc 0 in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
reconsider r = r as Element of NAT by ORDINAL1:def 12;
( dom (Start-At (((IC (Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),r))) + (card I)),SCM+FSA)) = {(IC )} & intloc 0 <> IC ) by SCMFSA_2:56;
then A11: not intloc 0 in dom (Start-At (((IC (Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),r))) + (card I)),SCM+FSA)) by TARSKI:def 1;
A12: IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),r)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + r)) by A4, Th16, A1;
A13: J c= (P +* I) +* J by FUNCT_4:25;
(Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),r)) . (intloc 0) = (Initialize (Result ((P +* I),s))) . (intloc 0) by Def2, A13
.= (Result ((P +* I),s)) . (intloc 0) by A10, FUNCT_4:11
.= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) . (intloc 0) by A4, EXTPRO_1:23
.= s . (intloc 0) by Def2, A2 ;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A7, A9, A12, A3, A11, FUNCT_4:11; :: thesis: verum

end;

end;

end;

end;

suppose A14: not P +* I halts_on s ; :: thesis: for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

let k be Nat; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
(Comput ((P +* I),s,k)) . (intloc 0) = s . (intloc 0) by Def2, A2;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A3, A14, Th15; :: thesis: verum

end;

end;