reconsider II = I as initial preProgram of SCM+FSA ;
let k1, k2 be Element of NAT ; :: thesis: ( IC (Comput ((P +* I),(Initialize s),k1)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
k1 <= n ) & IC (Comput ((P +* I),(Initialize s),k2)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
k2 <= n ) implies k1 = k2 )
assume that
A2: IC (Comput ((P +* I),(Initialize s),k1)) = card I and
A3: ( ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
k1 <= n ) & IC (Comput ((P +* I),(Initialize s),k2)) = card I ) and
A4: for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
k2 <= n ; :: thesis: k1 = k2

A5: now :: thesis: not k2 < k1

assume k2 < k1 ; :: thesis: contradiction
then card II in dom II by A3;
hence contradiction ; :: thesis: verum

end;

now :: thesis: not k1 < k2

assume k1 < k2 ; :: thesis: contradiction
then card II in dom II by A2, A4;
hence contradiction ; :: thesis: verum

end;

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