not product <% the carrier of N, the carrier of N%> is empty ;
hence not the carrier of (Cayley-Dickson N) is empty by Def9; :: according to STRUCT_0:def 1 :: thesis: verum