<%x%> = 0 .--> x by AFINSQ_1:def 1;
hence <%x%> is one-to-one ; :: thesis: verum