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 Element of 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 Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) )
assume A3: I ';' J c= P ; :: thesis: for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A4: I c= P +* I by FUNCT_4:25;
A5: P = P +* (I ';' J) by A3, FUNCT_4:98;

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

suppose A9: P +* I halts_on s ; :: thesis: for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

let k be Element of 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 A11: 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 Def4, A4;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A5, Th40, A9, A11; :: thesis: verum

end;

suppose A14: 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
A15: k = (LifeSpan ((P +* I),s)) + p and
A16: 1 <= p by A14, FINSEQ_4:84;
consider r being Nat such that
A17: p = 1 + r by A16, NAT_1:10;
( dom (Start-At (0,SCM+FSA)) = {(IC )} & intloc 0 <> IC ) by FUNCOP_1:13, SCMFSA_2:56;
then A18: 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 FUNCOP_1:13, SCMFSA_2:56;
then B19: 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;
A20: 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 A9, Th42, A3;
A22: 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 Def4, A22
.= (Result ((P +* I),s)) . (intloc 0) by A18, FUNCT_4:11
.= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) . (intloc 0) by A9, EXTPRO_1:23
.= s . (intloc 0) by Def4, A4 ;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A15, A17, A20, A5, B19, FUNCT_4:11; :: thesis: verum

end;

end;

end;

end;

suppose A24: not P +* I halts_on s ; :: thesis: for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

let k be Element of NAT ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
(Comput ((P +* I),s,k)) . (intloc 0) = s . (intloc 0) by Def4, A4;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A5, A24, Th41; :: thesis: verum

end;

end;