let c be Element of (Cayley-Dickson N); :: according to RLVECT_1:def 8 :: thesis: 1 * c = c
consider a, b being Element of N such that
A1: c = <%a,b%> by Th12;
( 1 * a = a & 1 * b = b ) by RLVECT_1:def 8;
hence 1 * c = c by A1, Def9; :: thesis: verum