let X be RealNormSpace; :: thesis: for Y being Subset of X

for f, g being Point of (ClNLin Y)

for a being Real holds

( ( ||.f.|| = 0 implies f = 0. (ClNLin Y) ) & ( f = 0. (ClNLin Y) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

let Y be Subset of X; :: thesis: for f, g being Point of (ClNLin Y)

for a being Real holds

( ( ||.f.|| = 0 implies f = 0. (ClNLin Y) ) & ( f = 0. (ClNLin Y) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

let f, g be Point of (ClNLin Y); :: thesis: for a being Real holds

( ( ||.f.|| = 0 implies f = 0. (ClNLin Y) ) & ( f = 0. (ClNLin Y) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

let a be Real; :: thesis: ( ( ||.f.|| = 0 implies f = 0. (ClNLin Y) ) & ( f = 0. (ClNLin Y) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

consider Z being Subset of X such that

A1: ( Z = the carrier of (Lin Y) & ClNLin Y = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) by defClN;

reconsider CL = Cl Z as Subset of X ;

reconsider f1 = f, g1 = g as Point of X by A1, TARSKI:def 3;

A3: f1 + g1 = f + g by SUBTHCL;

A4: a * f1 = a * f by SUBTHCL;

A5: ||.(f + g).|| = ||.(f1 + g1).|| by A3, SUBTHCL;

A6: ||.(a * f).|| = ||.(a * f1).|| by A4, SUBTHCL;

A7: ||.f.|| = ||.f1.|| by SUBTHCL;

A8: ||.g.|| = ||.g1.|| by SUBTHCL;

0. (ClNLin Y) = 0. X by A1, Cl01, RSSPACE:def 10;

hence ( ( ||.f.|| = 0 implies f = 0. (ClNLin Y) ) & ( f = 0. (ClNLin Y) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) by A5, A6, A7, A8, NORMSP_0:def 5, NORMSP_1:def 1; :: thesis: verum

for f, g being Point of (ClNLin Y)

for a being Real holds

( ( ||.f.|| = 0 implies f = 0. (ClNLin Y) ) & ( f = 0. (ClNLin Y) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

let Y be Subset of X; :: thesis: for f, g being Point of (ClNLin Y)

for a being Real holds

( ( ||.f.|| = 0 implies f = 0. (ClNLin Y) ) & ( f = 0. (ClNLin Y) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

let f, g be Point of (ClNLin Y); :: thesis: for a being Real holds

( ( ||.f.|| = 0 implies f = 0. (ClNLin Y) ) & ( f = 0. (ClNLin Y) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

let a be Real; :: thesis: ( ( ||.f.|| = 0 implies f = 0. (ClNLin Y) ) & ( f = 0. (ClNLin Y) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

consider Z being Subset of X such that

A1: ( Z = the carrier of (Lin Y) & ClNLin Y = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) by defClN;

reconsider CL = Cl Z as Subset of X ;

reconsider f1 = f, g1 = g as Point of X by A1, TARSKI:def 3;

A3: f1 + g1 = f + g by SUBTHCL;

A4: a * f1 = a * f by SUBTHCL;

A5: ||.(f + g).|| = ||.(f1 + g1).|| by A3, SUBTHCL;

A6: ||.(a * f).|| = ||.(a * f1).|| by A4, SUBTHCL;

A7: ||.f.|| = ||.f1.|| by SUBTHCL;

A8: ||.g.|| = ||.g1.|| by SUBTHCL;

0. (ClNLin Y) = 0. X by A1, Cl01, RSSPACE:def 10;

hence ( ( ||.f.|| = 0 implies f = 0. (ClNLin Y) ) & ( f = 0. (ClNLin Y) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) by A5, A6, A7, A8, NORMSP_0:def 5, NORMSP_1:def 1; :: thesis: verum