let N be 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%>%>
let c be Element of (Cayley-Dickson (Cayley-Dickson N)); 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
; ex b1, a2, b2 being Element of N st c = <%<%a1,b1%>,<%a2,b2%>%>
take
b1
; ex a2, b2 being Element of N st c = <%<%a1,b1%>,<%a2,b2%>%>
take
a2
; ex b2 being Element of N st c = <%<%a1,b1%>,<%a2,b2%>%>
take
b2
; c = <%<%a1,b1%>,<%a2,b2%>%>
thus
c = <%<%a1,b1%>,<%a2,b2%>%>
by A1, A2, A3; verum