let a be Real; :: thesis: for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, g being Point of (R_NormSpace_of_ContinuousFunctions (X,Y)) holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) ) & ( f = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
let X be non empty closed_interval Subset of REAL; :: thesis: for Y being RealNormSpace
for f, g being Point of (R_NormSpace_of_ContinuousFunctions (X,Y)) holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) ) & ( f = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
let Y be RealNormSpace; :: thesis: for f, g being Point of (R_NormSpace_of_ContinuousFunctions (X,Y)) holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) ) & ( f = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
let f, g be Point of (R_NormSpace_of_ContinuousFunctions (X,Y)); :: thesis: ( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) ) & ( f = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
reconsider f1 = f as VECTOR of (R_NormSpace_of_BoundedFunctions (X,Y)) by TARSKI:def 3;
reconsider g1 = g as VECTOR of (R_NormSpace_of_BoundedFunctions (X,Y)) by TARSKI:def 3;
A1: 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) = X --> (0. Y) by Th14
.= 0. (R_NormSpace_of_BoundedFunctions (X,Y)) by RSSPACE4:15 ;
A2: ||.(f1 + g1).|| <= ||.f1.|| + ||.g1.|| by RSSPACE4:21;
A3: ||.(f1 + g1).|| = ||.(f + g).|| by Th18, Th17;
A4: ||.f1.|| = ||.f.|| by FUNCT_1:49;
||.(a * f1).|| = ||.(a * f).|| by Th19, Th17;
hence ( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) ) & ( f = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) by RSSPACE4:21, A1, FUNCT_1:49, A2, A3, A4; :: thesis: verum