reconsider
b
=
b
as
Element
of
REAL
by
XREAL_0:def 1
;
NAT
-->
b
is
Real_Sequence
;
hence
NAT
-->
b
is
Real_Sequence
;
:: thesis:
verum