let r be Real; :: according to RLVECT_1:def 6 :: thesis: for b₁ being object
for b₂ being Element of the carrier of (Cayley-Dickson N) holds (r + b₁) * b₂ = (r * b₂) + (b₁ * b₂)
let s be Real; :: thesis: for b₁ being Element of the carrier of (Cayley-Dickson N) holds (r + s) * b₁ = (r * b₁) + (s * b₁)
let c be Element of (Cayley-Dickson N); :: thesis: (r + s) * c = (r * c) + (s * c)
consider a, b being Element of N such that
A1: c = <%a,b%> by Th12;
A2: ( (r + s) * a = (r * a) + (s * a) & (r + s) * b = (r * b) + (s * b) ) by RLVECT_1:def 6;
A3: ( r * <%a,b%> = <%(r * a),(r * b)%> & s * <%a,b%> = <%(s * a),(s * b)%> ) by Def9;
thus (r + s) * c = <%((r + s) * a),((r + s) * b)%> by A1, Def9
.= (r * c) + (s * c) by A1, A2, A3, Def9 ; :: thesis: verum