let N be non empty ConjNormAlgStr ; :: thesis: for c being Element of (Cayley-Dickson N) ex a, b being Element of N st c = <%a,b%>
let c be Element of (Cayley-Dickson N); :: thesis: ex a, b being Element of N st c = <%a,b%>
set C = Cayley-Dickson N;
the carrier of (Cayley-Dickson N) = product <% the carrier of N, the carrier of N%> by Def9;
then ex a, b being set st
( a in the carrier of N & b in the carrier of N & c = <%a,b%> ) by Th7;
hence ex a, b being Element of N st c = <%a,b%> ; :: thesis: verum