let r be Real; :: according to RLVECT_1:def 5 :: thesis: for b₁, b₂ being Element of the carrier of (Cayley-Dickson N) holds r * (b₁ + b₂) = (r * b₁) + (r * b₂)
let c1, c2 be Element of (Cayley-Dickson N); :: thesis: r * (c1 + c2) = (r * c1) + (r * c2)
consider a1, b1 being Element of N such that
A1: c1 = <%a1,b1%> by Th12;
consider a2, b2 being Element of N such that
A2: c2 = <%a2,b2%> by Th12;
A3: ( r * (a1 + a2) = (r * a1) + (r * a2) & r * (b1 + b2) = (r * b1) + (r * b2) ) by RLVECT_1:def 5;
A4: ( r * <%a1,b1%> = <%(r * a1),(r * b1)%> & r * <%a2,b2%> = <%(r * a2),(r * b2)%> ) by Def9;
c1 + c2 = <%(a1 + a2),(b1 + b2)%> by A1, A2, Def9;
hence r * (c1 + c2) = <%(r * (a1 + a2)),(r * (b1 + b2))%> by Def9
.= (r * c1) + (r * c2) by A1, A2, A3, A4, Def9 ;
:: thesis: verum