consider k being Element of NAT such that
A2: IC (Computation (s +* (P +* (Start-At (insloc 0 )))),k) = insloc (card (ProgramPart P)) and
A3: for n being Element of NAT st n < k holds
IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P by A1, Def3;
take k ; :: thesis: ( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),k) = insloc (card (ProgramPart P)) & ( for n being Element of NAT st not IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P holds
k <= n ) )
thus ( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),k) = insloc (card (ProgramPart P)) & ( for n being Element of NAT st not IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P holds
k <= n ) ) by A2, A3; :: thesis: verum