let r be Real; :: according to CAYLDICK:def 7 :: thesis: for a being Element of (Cayley-Dickson N) holds r * (a *') = (r * a) *'
let a be Element of (Cayley-Dickson N); :: thesis: r * (a *') = (r * a) *'
consider a1, a2 being Element of N such that
A1: a = <%a1,a2%> by Th12;
A2: r * (- a2) = - (r * a2) by RLVECT_1:25;
r * a = <%(r * a1),(r * a2)%> by A1, Def9;
then A3: (r * a) *' = <%((r * a1) *'),(- (r * a2))%> by Def9;
A4: r * (a1 *') = (r * a1) *' by Def7;
a *' = <%(a1 *'),(- a2)%> by A1, Def9;
hence (r * a) *' = r * (a *') by A2, A3, A4, Def9; :: thesis: verum