consider k being Nat such that

A2: ( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Nat st n < k holds

IC (Comput ((P +* I),(Initialize s),n)) in dom I ) ) by A1;

take k ; :: thesis: ( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being 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 Nat st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds

k <= n ) ) by A2; :: thesis: verum

A2: ( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Nat st n < k holds

IC (Comput ((P +* I),(Initialize s),n)) in dom I ) ) by A1;

take k ; :: thesis: ( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being 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 Nat st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds

k <= n ) ) by A2; :: thesis: verum