consider k being Element of NAT such that
A1: ( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Element of NAT st n < k holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) ) by X1, Def2;
take k ; :: thesis: ( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
k <= n ) )
thus ( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
k <= n ) ) by A1; :: thesis: verum