let k1, k2 be Element of NAT ; :: thesis: ( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),k1) = 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
k1 <= n ) & IC (Computation (s +* (P +* (Start-At (insloc 0 )))),k2) = 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
k2 <= n ) implies k1 = k2 )
assume that
A4: IC (Computation (s +* (P +* (Start-At (insloc 0 )))),k1) = insloc (card (ProgramPart P)) and
A5: for n being Element of NAT st not IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P holds
k1 <= n and
A6: IC (Computation (s +* (P +* (Start-At (insloc 0 )))),k2) = insloc (card (ProgramPart P)) and
A7: for n being Element of NAT st not IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P holds
k2 <= n ; :: thesis: k1 = k2
reconsider I = [(ProgramPart P)] as Program of SCM+FSA ;

A8: now

assume k1 < k2 ; :: thesis: contradiction
then insloc (card I) in dom I by A4, A7, AMI_1:106;
hence contradiction by SCMFSA6A:15; :: thesis: verum

end;

now

assume k2 < k1 ; :: thesis: contradiction
then insloc (card I) in dom I by A5, A6, AMI_1:106;
hence contradiction by SCMFSA6A:15; :: thesis: verum

end;

hence k1 = k2 by A8, XXREAL_0:1; :: thesis: verum