let X, Y, Z be RealNormSpace; 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))
; verum