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