let a, b be Element of (Cayley-Dickson N); CAYLDICK:def 5 (a + b) *' = (a *') + (b *')
consider a1, a2 being Element of N such that
A1:
a = <%a1,a2%>
by Th12;
consider b1, b2 being Element of N such that
A2:
b = <%b1,b2%>
by Th12;
A3:
(a1 + b1) *' = (a1 *') + (b1 *')
by Def5;
A4:
( a *' = <%(a1 *'),(- a2)%> & b *' = <%(b1 *'),(- b2)%> )
by A1, A2, Def9;
A5:
- (a2 + b2) = (- a2) - b2
by RLVECT_1:30;
a + b = <%(a1 + b1),(a2 + b2)%>
by A1, A2, Def9;
hence (a + b) *' =
<%((a1 + b1) *'),(- (a2 + b2))%>
by Def9
.=
(a *') + (b *')
by A3, A4, A5, Def9
;
verum