let X, Y, Z be RealNormSpace; for z being object holds
( z in BilinearOperators (X,Y,Z) iff z is BilinearOperator of X,Y,Z )
let z be object ; ( z in BilinearOperators (X,Y,Z) iff z is BilinearOperator of X,Y,Z )
reconsider X0 = X, Y0 = Y, Z0 = Z as RealLinearSpace ;
hereby ( z is BilinearOperator of X,Y,Z implies z in BilinearOperators (X,Y,Z) )
assume
z in BilinearOperators (
X,
Y,
Z)
;
z is BilinearOperator of X,Y,Zthen
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;
verum
end;
assume
z is BilinearOperator of X,Y,Z
; 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; verum