theorem Th13: :: CAYLDICK:13

for N being non empty ConjNormAlgStr
for c being Element of (Cayley-Dickson (Cayley-Dickson N)) ex a1, b1, a2, b2 being Element of N st c = <%<%a1,b1%>,<%a2,b2%>%>