`lim[x->oo] sin(x)` returns a number (the limit does not exist!)

[jackmaney]

Hi guys,thank you for using Hilbert.
You need to execute "postulate zfc_analysis" if you wanna do real analysis.

Enjoy! -> postulate zfc_analysis
success! :)
Enjoy! -> lim[x->oo] sin(x)
0.03574879797201651

Since the set of x such that sin(x) == 1 and the set of x such that sin(x) == -1 are both unbounded, it follows that this limit cannot possibly exist.