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
proof
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;
then f is Lipschitzian by Th21;
hence not BoundedBilinearOperators (X,Y,Z) is empty by Def9; :: thesis: verum