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