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 ;

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

( 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 is BilinearOperator of X,Y,Z
; :: thesis: 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;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

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