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