set C = Cayley-Dickson N;
let a be Element of (Cayley-Dickson N); :: according to VECTSP_1:def 6 :: thesis: ( a * (1. (Cayley-Dickson N)) = a & (1. (Cayley-Dickson N)) * a = a )
consider a1, b1 being Element of N such that
A1: a = <%a1,b1%> by Th12;
A2: ( a1 * (1. N) = a1 & (1. N) * a1 = a1 & b1 * (1. N) = b1 ) by VECTSP_1:def 6;
A3: 1. (Cayley-Dickson N) = <%(1. N),(0. N)%> by Def9;
then A4: a * (1. (Cayley-Dickson N)) = <%((a1 * (1. N)) - (((0. N) *') * b1)),(((0. N) * a1) + (b1 * ((1. N) *')))%> by A1, Def9;
(1. (Cayley-Dickson N)) * a = <%(((1. N) * a1) - ((b1 *') * (0. N))),((b1 * (1. N)) + ((0. N) * (a1 *')))%> by A1, A3, Def9;
hence ( a * (1. (Cayley-Dickson N)) = a & (1. (Cayley-Dickson N)) * a = a ) by A1, A2, A4; :: thesis: verum