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

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

assume A1: for x being VECTOR of X
for y being VECTOR of Y holds f . (x,y) = 0. Z ; :: thesis: f is Lipschitzian
A2: now :: thesis: for x being VECTOR of X
for y being VECTOR of Y holds ||.(f . (x,y)).|| = () *
let x be VECTOR of X; :: thesis: for y being VECTOR of Y holds ||.(f . (x,y)).|| = () *
let y be VECTOR of Y; :: thesis: ||.(f . (x,y)).|| = () *
thus ||.(f . (x,y)).|| = ||.(0. Z).|| by A1
.= () * ; :: thesis: verum
end;
take 0 ; :: according to LOPBAN_9:def 3 :: thesis: ( 0 <= 0 & ( for x being VECTOR of X
for y being VECTOR of Y holds ||.(f . (x,y)).|| <= () * ) )

thus ( 0 <= 0 & ( for x being VECTOR of X
for y being VECTOR of Y holds ||.(f . (x,y)).|| <= () * ) ) by A2; :: thesis: verum