let N be non empty ConjNormAlgStr ; :: thesis: 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%>%>
let c be Element of (Cayley-Dickson (Cayley-Dickson N)); :: thesis: ex a1, b1, a2, b2 being Element of N st c = <%<%a1,b1%>,<%a2,b2%>%>
consider a, b being Element of (Cayley-Dickson N) such that
A1: c = <%a,b%> by Th12;
consider a1, b1 being Element of N such that
A2: a = <%a1,b1%> by Th12;
consider a2, b2 being Element of N such that
A3: b = <%a2,b2%> by Th12;
take a1 ; :: thesis: ex b1, a2, b2 being Element of N st c = <%<%a1,b1%>,<%a2,b2%>%>
take b1 ; :: thesis: ex a2, b2 being Element of N st c = <%<%a1,b1%>,<%a2,b2%>%>
take a2 ; :: thesis: ex b2 being Element of N st c = <%<%a1,b1%>,<%a2,b2%>%>
take b2 ; :: thesis: c = <%<%a1,b1%>,<%a2,b2%>%>
thus c = <%<%a1,b1%>,<%a2,b2%>%> by A1, A2, A3; :: thesis: verum