let a, b be Element of (Cayley-Dickson N); :: according to CAYLDICK:def 5 :: thesis: (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 ;
:: thesis: verum