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