reconsider I = ProgramPart P as Program of SCM+FSA ;
let k1, k2 be Element of NAT ; :: thesis: ( IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),k1) = 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
k1 <= n ) & IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),k2) = 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
k2 <= n ) implies k1 = k2 )
assume that
A3: IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),k1) = card (ProgramPart P) and
A4: ( ( 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
k1 <= n ) & IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),k2) = card (ProgramPart P) ) and
A5: 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
k2 <= n ; :: thesis: k1 = k2

A6: now

assume k2 < k1 ; :: thesis: contradiction
then card I in dom I by A4, COMPOS_1:16;
hence contradiction ; :: thesis: verum

end;

now

assume k1 < k2 ; :: thesis: contradiction
then card I in dom I by A3, A5, COMPOS_1:16;
hence contradiction ; :: thesis: verum

end;

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