let X be non empty set ; for a being Real
for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let a be Real; for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let F, G be Point of (R_Normed_Algebra_of_BoundedFunctions X); ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
A1:
now ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 )set z =
X --> (In (0,REAL));
reconsider z =
X --> (In (0,REAL)) as
Function of
X,
REAL ;
F in BoundedFunctions X
;
then consider g being
Function of
X,
REAL such that A2:
F = g
and A3:
g | X is
bounded
;
A4:
( not
PreNorms g is
empty &
PreNorms g is
bounded_above )
by A3, Th17;
consider r0 being
object such that A5:
r0 in PreNorms g
by XBOOLE_0:def 1;
reconsider r0 =
r0 as
Real by A5;
A6:
( ( for
s being
Real st
s in PreNorms g holds
s <= 0 ) implies
upper_bound (PreNorms g) <= 0 )
by SEQ_4:45;
assume
F = 0. (R_Normed_Algebra_of_BoundedFunctions X)
;
||.F.|| = 0 then A7:
z = g
by A2, Th25;
then
0 <= r0
by A5;
then
upper_bound (PreNorms g) = 0
by A8, A4, A5, A6, SEQ_4:def 1;
hence
||.F.|| = 0
by A2, A3, Th20;
verum end;
A10:
||.(F + G).|| <= ||.F.|| + ||.G.||
A20:
||.(a * F).|| = |.a.| * ||.F.||
hence
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
by A1, A20, A10; verum