<%A,x%> . 0 = A ;
hence not <%A,x%> is natural-valued ; :: thesis: verum