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
hence n1 = n2 ; :: thesis: verum