let c1, c2 be Element of (Cayley-Dickson N); :: according to NORMSP_1:def 1 :: thesis: for b₁ being object holds
( ||.(b₁ * c1).|| = |.b₁.| * ||.c1.|| & ||.(c1 + c2).|| <= ||.c1.|| + ||.c2.|| )
let r be Real; :: thesis: ( ||.(r * c1).|| = |.r.| * ||.c1.|| & ||.(c1 + c2).|| <= ||.c1.|| + ||.c2.|| )
consider a1, b1 being Element of N such that
A1: c1 = <%a1,b1%> by Th12;
A2: r * c1 = <%(r * a1),(r * b1)%> by A1, Def9;
A3: ( ||.(r * a1).|| = |.r.| * ||.a1.|| & ||.(r * b1).|| = |.r.| * ||.b1.|| ) by NORMSP_1:def 1;
thus ||.(r * c1).|| = sqrt ((||.(r * a1).|| ^2) + (||.(r * b1).|| ^2)) by A2, Def9
.= sqrt ((|.r.| ^2) * ((||.a1.|| ^2) + (||.b1.|| ^2))) by A3
.= |.r.| * (sqrt ((||.a1.|| ^2) + (||.b1.|| ^2))) by SQUARE_1:54
.= |.r.| * ||.c1.|| by A1, Def9 ; :: thesis: ||.(c1 + c2).|| <= ||.c1.|| + ||.c2.||
consider a2, b2 being Element of N such that
A4: c2 = <%a2,b2%> by Th12;
set A1 = ||.a1.||;
set A2 = ||.a2.||;
set B1 = ||.b1.||;
set B2 = ||.b2.||;
set C1 = ||.c1.||;
set C2 = ||.c2.||;
( ||.(a1 + a2).|| <= ||.a1.|| + ||.a2.|| & ||.(b1 + b2).|| <= ||.b1.|| + ||.b2.|| ) by NORMSP_1:def 1;
then ( ||.(a1 + a2).|| ^2 <= (||.a1.|| + ||.a2.||) ^2 & ||.(b1 + b2).|| ^2 <= (||.b1.|| + ||.b2.||) ^2 ) by XREAL_1:66;
then A5: (||.(a1 + a2).|| ^2) + (||.(b1 + b2).|| ^2) <= ((||.a1.|| + ||.a2.||) ^2) + ((||.b1.|| + ||.b2.||) ^2) by XREAL_1:7;
c1 + c2 = <%(a1 + a2),(b1 + b2)%> by A1, A4, Def9;
then A6: ||.(c1 + c2).|| = sqrt ((||.(a1 + a2).|| ^2) + (||.(b1 + b2).|| ^2)) by Def9;
A7: ( ||.c1.|| = sqrt ((||.a1.|| ^2) + (||.b1.|| ^2)) & ||.c2.|| = sqrt ((||.a2.|| ^2) + (||.b2.|| ^2)) ) by A1, A4, Def9;
then ( 0 <= ||.c1.|| & 0 <= ||.c2.|| ) by SQUARE_1:def 2;
then A8: ||.c1.|| + ||.c2.|| = sqrt ((||.c1.|| + ||.c2.||) ^2) by SQUARE_1:def 2;
((||.a1.|| + ||.a2.||) ^2) + ((||.b1.|| + ||.b2.||) ^2) <= (||.c1.|| + ||.c2.||) ^2 by A7, Th1;
then (||.(a1 + a2).|| ^2) + (||.(b1 + b2).|| ^2) <= (||.c1.|| + ||.c2.||) ^2 by A5, XXREAL_0:2;
hence ||.(c1 + c2).|| <= ||.c1.|| + ||.c2.|| by A6, A8, SQUARE_1:26; :: thesis: verum