let X, Y, Z be RealNormSpace; :: thesis: ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is reflexive & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is discerning & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealNormSpace-like )

thus ||.(0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))).|| = 0 by Th37; :: according to NORMSP_0:def 6 :: thesis: ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is discerning & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealNormSpace-like )

for x, y being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))

for a being Real holds

( ( ||.x.|| = 0 implies x = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ) & ( x = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th37;

hence ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is discerning & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealNormSpace-like ) by NORMSP_1:def 1, NORMSP_0:def 5; :: thesis: verum

thus ||.(0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))).|| = 0 by Th37; :: according to NORMSP_0:def 6 :: thesis: ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is discerning & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealNormSpace-like )

for x, y being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))

for a being Real holds

( ( ||.x.|| = 0 implies x = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ) & ( x = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th37;

hence ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is discerning & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealNormSpace-like ) by NORMSP_1:def 1, NORMSP_0:def 5; :: thesis: verum