let X, Y be ComplexNormSpace; :: thesis: the carrier of X --> (0. Y) = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y))

the carrier of X --> (0. Y) = 0. (C_VectorSpace_of_BoundedLinearOperators (X,Y)) by Th25

.= 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ;

hence the carrier of X --> (0. Y) = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ; :: thesis: verum

the carrier of X --> (0. Y) = 0. (C_VectorSpace_of_BoundedLinearOperators (X,Y)) by Th25

.= 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ;

hence the carrier of X --> (0. Y) = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ; :: thesis: verum