let X, Y, Z be RealNormSpace; :: thesis: for z being object holds
( z in BilinearOperators (X,Y,Z) iff z is BilinearOperator of X,Y,Z )
let z be object ; :: thesis: ( z in BilinearOperators (X,Y,Z) iff z is BilinearOperator of X,Y,Z )
reconsider X0 = X, Y0 = Y, Z0 = Z as RealLinearSpace ;

hereby :: thesis: ( z is BilinearOperator of X,Y,Z implies z in BilinearOperators (X,Y,Z) )

assume z in BilinearOperators (X,Y,Z) ; :: thesis: z is BilinearOperator of X,Y,Z
then z is BilinearOperator of X0,Y0,Z0 by Def6;
then consider g being Function of [: the carrier of X0, the carrier of Y0:], the carrier of Z0 such that
A1: ( z = g & g is Bilinear ) by LOPBAN_8:def 2;
thus z is BilinearOperator of X,Y,Z by A1, LOPBAN_8:def 3; :: thesis: verum

end;

assume z is BilinearOperator of X,Y,Z ; :: thesis: z in BilinearOperators (X,Y,Z)
then consider g being Function of [: the carrier of X, the carrier of Y:], the carrier of Z such that
A1: ( z = g & g is Bilinear ) by LOPBAN_8:def 3;
reconsider w = g as BilinearOperator of X0,Y0,Z0 by LOPBAN_8:def 2, A1;
w in BilinearOperators (X,Y,Z) by Def6;
hence z in BilinearOperators (X,Y,Z) by A1; :: thesis: verum