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