reconsider f = id NAT as sequence of REAL by FUNCT_2:7, NUMBERS:19;
f is AP-like ;
hence ex b₁ being sequence of REAL st b₁ is AP-like ; :: thesis: verum