let V be RealNormSpace; :: thesis: for V1 being Subset of V
for x, y being Point of (NLin V1)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (NLin V1) ) & ( x = 0. (NLin V1) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
let V1 be Subset of V; :: thesis: for x, y being Point of (NLin V1)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (NLin V1) ) & ( x = 0. (NLin V1) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
let x, y be Point of (NLin V1); :: thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (NLin V1) ) & ( x = 0. (NLin V1) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
let a be Real; :: thesis: ( ( ||.x.|| = 0 implies x = 0. (NLin V1) ) & ( x = 0. (NLin V1) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
set l = NLin V1;
the carrier of (NLin V1) c= the carrier of V by RLSUB_1:def 2;
then reconsider x0 = x, y0 = y as Point of V ;
A1: ||.x.|| = ||.x0.|| by SUBTH;
A2: ||.y.|| = ||.y0.|| by SUBTH;
A3: 0. (NLin V1) = 0. V by RLSUB_1:11;
x + y = x0 + y0 by SUBTH;
then A4: ||.(x0 + y0).|| = ||.(x + y).|| by SUBTH;
a * x = a * x0 by SUBTH;
then A5: ||.(a * x0).|| = ||.(a * x).|| by SUBTH;
thus ( ||.x.|| = 0 iff x = 0. (NLin V1) ) by A1, A3, NORMSP_0:def 5; :: thesis: ( 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
thus 0 <= ||.x.|| by A1; :: thesis: ( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
thus ||.(x + y).|| <= ||.x.|| + ||.y.|| by A1, A2, A4, NORMSP_1:def 1; :: thesis: ||.(a * x).|| = |.a.| * ||.x.||
thus ||.(a * x).|| = |.a.| * ||.x.|| by A1, A5, NORMSP_1:def 1; :: thesis: verum