let X, Y, Z be RealLinearSpace; :: thesis: 0. (R_VectorSpace_of_BilinearOperators (X,Y,Z)) = the carrier of [:X,Y:] --> (0. Z)

A1: 0. (RealVectSpace ( the carrier of [:X,Y:],Z)) = the carrier of [:X,Y:] --> (0. Z) ;

R_VectorSpace_of_BilinearOperators (X,Y,Z) is Subspace of RealVectSpace ( the carrier of [:X,Y:],Z) by RSSPACE:11;

hence 0. (R_VectorSpace_of_BilinearOperators (X,Y,Z)) = the carrier of [:X,Y:] --> (0. Z) by A1, RLSUB_1:11; :: thesis: verum

A1: 0. (RealVectSpace ( the carrier of [:X,Y:],Z)) = the carrier of [:X,Y:] --> (0. Z) ;

R_VectorSpace_of_BilinearOperators (X,Y,Z) is Subspace of RealVectSpace ( the carrier of [:X,Y:],Z) by RSSPACE:11;

hence 0. (R_VectorSpace_of_BilinearOperators (X,Y,Z)) = the carrier of [:X,Y:] --> (0. Z) by A1, RLSUB_1:11; :: thesis: verum