let X be RealNormSpace; :: thesis: for Y being Subset of X
for f, g being Point of ()
for a being Real holds
( ( = 0 implies f = 0. () ) & ( f = 0. () implies = 0 ) & ||.(a * f).|| = |.a.| * & ||.(f + g).|| <= + )

let Y be Subset of X; :: thesis: for f, g being Point of ()
for a being Real holds
( ( = 0 implies f = 0. () ) & ( f = 0. () implies = 0 ) & ||.(a * f).|| = |.a.| * & ||.(f + g).|| <= + )

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

let a be Real; :: thesis: ( ( = 0 implies f = 0. () ) & ( f = 0. () implies = 0 ) & ||.(a * f).|| = |.a.| * & ||.(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 ;
A3: f1 + g1 = f + g by SUBTHCL;
A4: a * f1 = a * f by SUBTHCL;
A5: ||.(f + g).|| = ||.(f1 + g1).|| by ;
A6: ||.(a * f).|| = ||.(a * f1).|| by ;
A7: ||.f.|| = ||.f1.|| by SUBTHCL;
A8: ||.g.|| = ||.g1.|| by SUBTHCL;
0. () = 0. X by ;
hence ( ( ||.f.|| = 0 implies f = 0. () ) & ( f = 0. () implies = 0 ) & ||.(a * f).|| = |.a.| * & ||.(f + g).|| <= + ) by ; :: thesis: verum