let X, Y be RealNormSpace; :: thesis: the carrier of X --> (0. Y) = 0. (R_NormSpace_of_BoundedLinearOperators X,Y)
the carrier of X --> (0. Y) = 0. (R_VectorSpace_of_BoundedLinearOperators X,Y) by Th31
.= 0. (R_NormSpace_of_BoundedLinearOperators X,Y) ;
hence the carrier of X --> (0. Y) = 0. (R_NormSpace_of_BoundedLinearOperators X,Y) ; :: thesis: verum