let X, Y, Z be RealNormSpace; for f being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds 0 <= ||.f.||
let f be Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)); 0 <= ||.f.||
reconsider g = f as Lipschitzian BilinearOperator of X,Y,Z by Def9;
consider r0 being object such that
A1:
r0 in PreNorms g
by XBOOLE_0:def 1;
reconsider r0 = r0 as Real by A1;
A3:
(BoundedBilinearOperatorsNorm (X,Y,Z)) . f = upper_bound (PreNorms g)
by Th30;
then
0 <= r0
by A1;
hence
0 <= ||.f.||
by A1, A3, SEQ_4:def 1; verum