set f = choice_succ_func w,v,U;
let n1, n2 be Nat; :: thesis: ( ( for i being Nat st i < n1 holds
( not CastNode (((choice_succ_func w,v,U) |** i) . N),v is elementary & CastNode (((choice_succ_func w,v,U) |** (i + 1)) . N),v is_succ_of CastNode (((choice_succ_func w,v,U) |** i) . N),v ) ) & CastNode (((choice_succ_func w,v,U) |** n1) . N),v is elementary & ( for i being Nat st i <= n1 holds
w |= * (CastNode (((choice_succ_func w,v,U) |** i) . N),v) ) & ( for i being Nat st i < n2 holds
( not CastNode (((choice_succ_func w,v,U) |** i) . N),v is elementary & CastNode (((choice_succ_func w,v,U) |** (i + 1)) . N),v is_succ_of CastNode (((choice_succ_func w,v,U) |** i) . N),v ) ) & CastNode (((choice_succ_func w,v,U) |** n2) . N),v is elementary & ( for i being Nat st i <= n2 holds
w |= * (CastNode (((choice_succ_func w,v,U) |** i) . N),v) ) implies n1 = n2 )
assume that
A4: for i being Nat st i < n1 holds
( not CastNode (((choice_succ_func w,v,U) |** i) . N),v is elementary & CastNode (((choice_succ_func w,v,U) |** (i + 1)) . N),v is_succ_of CastNode (((choice_succ_func w,v,U) |** i) . N),v ) and
A5: CastNode (((choice_succ_func w,v,U) |** n1) . N),v is elementary and
for i being Nat st i <= n1 holds
w |= * (CastNode (((choice_succ_func w,v,U) |** i) . N),v) and
A6: for i being Nat st i < n2 holds
( not CastNode (((choice_succ_func w,v,U) |** i) . N),v is elementary & CastNode (((choice_succ_func w,v,U) |** (i + 1)) . N),v is_succ_of CastNode (((choice_succ_func w,v,U) |** i) . N),v ) and
A7: CastNode (((choice_succ_func w,v,U) |** n2) . N),v is elementary and
for i being Nat st i <= n2 holds
w |= * (CastNode (((choice_succ_func w,v,U) |** i) . N),v) ; :: thesis: n1 = n2

now

assume A8: n1 <> n2 ; :: thesis: contradiction

now

per cases ( n1 < n2 or n2 < n1 ) by A8, XXREAL_0:1;

suppose n1 < n2 ; :: thesis: contradiction

hence contradiction by A5, A6; :: thesis: verum

end;

suppose n2 < n1 ; :: thesis: contradiction

hence contradiction by A4, A7; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence n1 = n2 ; :: thesis: verum