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;

take f ; :: thesis: f is Lipschitzian

for x being VECTOR of X

for y being VECTOR of Y holds f . (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;

take f ; :: thesis: f is Lipschitzian

for x being VECTOR of X

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

proof

hence
f is Lipschitzian
by Th21; :: thesis: verum
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