<%a,b%> in product <% the carrier of N, the carrier of N%> by Th6;
hence <%a,b%> is Element of (Cayley-Dickson N) by Def9; :: thesis: verum