let c1, c2 be Element of (Cayley-Dickson N); NORMSP_1:def 1 for b1 being object holds
( ||.(b1 * c1).|| = |.b1.| * ||.c1.|| & ||.(c1 + c2).|| <= ||.c1.|| + ||.c2.|| )
let r be Real; ( ||.(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
; ||.(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; verum