theorem Th12: :: CAYLDICK:12

for N being non empty ConjNormAlgStr
for c being Element of (Cayley-Dickson N) ex a, b being Element of N st c = <%a,b%>