seq_const 0 is negligible ;
hence ex b₁ being Function of NAT,REAL st b₁ is negligible ; :: thesis: verum