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

for y being VECTOR of Y holds ||.(f . (x,y)).|| <= (0 * ||.x.||) * ||.y.|| ) )

thus ( 0 <= 0 & ( for x being VECTOR of X

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

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)).|| = (0 * ||.x.||) * ||.y.||

take
0
; :: according to LOPBAN_9:def 3 :: thesis: ( 0 <= 0 & ( for x being VECTOR of Xfor y being VECTOR of Y holds ||.(f . (x,y)).|| = (0 * ||.x.||) * ||.y.||

let x be VECTOR of X; :: thesis: for y being VECTOR of Y holds ||.(f . (x,y)).|| = (0 * ||.x.||) * ||.y.||

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

thus ||.(f . (x,y)).|| = ||.(0. Z).|| by A1

.= (0 * ||.x.||) * ||.y.|| ; :: thesis: verum

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

thus ||.(f . (x,y)).|| = ||.(0. Z).|| by A1

.= (0 * ||.x.||) * ||.y.|| ; :: thesis: verum

for y being VECTOR of Y holds ||.(f . (x,y)).|| <= (0 * ||.x.||) * ||.y.|| ) )

thus ( 0 <= 0 & ( for x being VECTOR of X

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