let X, Y, Z be RealNormSpace; :: thesis: the carrier of [:X,Y:] --> (0. Z) = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))
the carrier of [:X,Y:] --> (0. Z) = 0. (R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) by Th26
.= 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ;
hence the carrier of [:X,Y:] --> (0. Z) = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ; :: thesis: verum