let a be Real; 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; 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; 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)); ( ( ||.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; verum