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

reconsider f = the carrier of [:X,Y:] --> (0. Z) as BilinearOperator of X,Y,Z by LOPBAN_8:9, LOPBAN_8:def 3;

for x being VECTOR of X

for y being VECTOR of Y holds f . (x,y) = 0. Z

hence not BoundedBilinearOperators (X,Y,Z) is empty by Def9; :: thesis: verum

reconsider f = the carrier of [:X,Y:] --> (0. Z) as BilinearOperator of X,Y,Z by LOPBAN_8:9, LOPBAN_8:def 3;

for x being VECTOR of X

for y being VECTOR of Y holds f . (x,y) = 0. Z

proof

then
f is Lipschitzian
by Th21;
let x be VECTOR of X; :: thesis: for y being VECTOR of Y holds f . (x,y) = 0. Z

let y be VECTOR of Y; :: thesis: f . (x,y) = 0. Z

[x,y] is Point of [:X,Y:] ;

hence f . (x,y) = 0. Z by FUNCOP_1:7; :: thesis: verum

end;let y be VECTOR of Y; :: thesis: f . (x,y) = 0. Z

[x,y] is Point of [:X,Y:] ;

hence f . (x,y) = 0. Z by FUNCOP_1:7; :: thesis: verum

hence not BoundedBilinearOperators (X,Y,Z) is empty by Def9; :: thesis: verum