let V be RealNormSpace; :: thesis: for V1 being Subset of V
for x, y being Point of (NLin V1)
for a being Real holds
( ( = 0 implies x = 0. (NLin V1) ) & ( x = 0. (NLin V1) implies = 0 ) & 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )

let V1 be Subset of V; :: thesis: for x, y being Point of (NLin V1)
for a being Real holds
( ( = 0 implies x = 0. (NLin V1) ) & ( x = 0. (NLin V1) implies = 0 ) & 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )

let x, y be Point of (NLin V1); :: thesis: for a being Real holds
( ( = 0 implies x = 0. (NLin V1) ) & ( x = 0. (NLin V1) implies = 0 ) & 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )

let a be Real; :: thesis: ( ( = 0 implies x = 0. (NLin V1) ) & ( x = 0. (NLin V1) implies = 0 ) & 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )
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 ; :: thesis: ( 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )
thus 0 <= by A1; :: thesis: ( ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )
thus ||.(x + y).|| <= + by ; :: thesis: ||.(a * x).|| = |.a.| *
thus ||.(a * x).|| = |.a.| * by ; :: thesis: verum