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

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