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

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