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 :: thesis: not n1 <> n2

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

now :: thesis: contradiction

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