:: deftheorem Def9 defines Cayley-Dickson CAYLDICK:def 9 :
for N being non empty ConjNormAlgStr
for b₂ being strict ConjNormAlgStr holds
( b₂ = Cayley-Dickson N iff ( the carrier of b₂ = product <% the carrier of N, the carrier of N%> & the ZeroF of b₂ = <%(0. N),(0. N)%> & the OneF of b₂ = <%(1. N),(0. N)%> & ( for a1, a2, b1, b2 being Element of N holds
( the addF of b₂ . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of b₂ . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> ) ) & ( for r being Real
for a, b being Element of N holds the Mult of b₂ . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of b₂ . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of b₂ . <%a,b%> = <%(a *'),(- b)%> ) ) ) );