take NAT --> rr ; :: thesis: NAT --> rr is polynomially-abs-bounded
thus NAT --> rr is polynomially-abs-bounded by LM1; :: thesis: verum