let X, Y, Z be RealNormSpace; :: thesis: for g being BilinearOperator of X,Y,Z holds
( g is Lipschitzian iff PreNorms g is bounded_above )
let g be BilinearOperator of X,Y,Z; :: thesis: ( g is Lipschitzian iff PreNorms g is bounded_above )

now :: thesis: ( PreNorms g is bounded_above implies ex K being Real st g is Lipschitzian )

reconsider K = upper_bound (PreNorms g) as Real ;
assume A1: PreNorms g is bounded_above ; :: thesis: ex K being Real st g is Lipschitzian

A2: now :: thesis: for t being VECTOR of X
for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||

let t be VECTOR of X; :: thesis: for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||
let s be VECTOR of Y; :: thesis: ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||

now :: thesis: ( ( ( t = 0. X or s = 0. Y ) & ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.|| ) or ( t <> 0. X & s <> 0. Y & ||.(g . (t,s)).|| <= K * (||.t.|| * ||.s.||) ) )

per cases ( t = 0. X or s = 0. Y or ( t <> 0. X & s <> 0. Y ) ) ;

case A3: ( t = 0. X or s = 0. Y ) ; :: thesis: ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||

then A4: ( ||.t.|| = 0 or ||.s.|| = 0 ) ;
( t = 0 * t or s = 0 * s ) by A3;
then g . (t,s) = 0 * (g . (t,s)) by LOPBAN_8:12
.= 0. Z by RLVECT_1:10 ;
hence ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.|| by A4; :: thesis: verum

end;

case A5: ( t <> 0. X & s <> 0. Y ) ; :: thesis: ||.(g . (t,s)).|| <= K * (||.t.|| * ||.s.||)

reconsider t1 = (||.t.|| ") * t as VECTOR of X ;
reconsider s1 = (||.s.|| ") * s as VECTOR of Y ;
A6: ( ||.t.|| <> 0 & ||.s.|| <> 0 ) by A5, NORMSP_0:def 5;
then A7: ||.t.|| * ||.s.|| <> 0 by XCMPLX_1:6;
A8: (||.(g . (t,s)).|| / (||.t.|| * ||.s.||)) * (||.t.|| * ||.s.||) = (||.(g . (t,s)).|| * ((||.t.|| * ||.s.||) ")) * (||.t.|| * ||.s.||) by XCMPLX_0:def 9
.= ||.(g . (t,s)).|| * (((||.t.|| * ||.s.||) ") * (||.t.|| * ||.s.||))
.= ||.(g . (t,s)).|| * 1 by A7, XCMPLX_0:def 7
.= ||.(g . (t,s)).|| ;
A9: |.(||.t.|| ").| = |.(1 * (||.t.|| ")).|
.= |.(1 / ||.t.||).| by XCMPLX_0:def 9
.= 1 / ||.t.|| by ABSVALUE:def 1
.= 1 * (||.t.|| ") by XCMPLX_0:def 9
.= ||.t.|| " ;
A10: |.(||.s.|| ").| = |.(1 * (||.s.|| ")).|
.= |.(1 / ||.s.||).| by XCMPLX_0:def 9
.= 1 / ||.s.|| by ABSVALUE:def 1
.= 1 * (||.s.|| ") by XCMPLX_0:def 9
.= ||.s.|| " ;
A11: |.((||.t.|| * ||.s.||) ").| = |.((||.t.|| ") * (||.s.|| ")).| by XCMPLX_1:204
.= (||.t.|| ") * (||.s.|| ") by A9, A10, COMPLEX1:65
.= (||.t.|| * ||.s.||) " by XCMPLX_1:204 ;
A12: ||.t1.|| = |.(||.t.|| ").| * ||.t.|| by NORMSP_1:def 1
.= 1 by A6, A9, XCMPLX_0:def 7 ;
||.s1.|| = |.(||.s.|| ").| * ||.s.|| by NORMSP_1:def 1
.= 1 by A6, A10, XCMPLX_0:def 7 ;
then A13: ||.(g . (t1,s1)).|| in { ||.(g . (t,s)).|| where t is VECTOR of X, s is VECTOR of Y : ( ||.t.|| <= 1 & ||.s.|| <= 1 ) } by A12;
||.(g . (t,s)).|| / (||.t.|| * ||.s.||) = ||.(g . (t,s)).|| * ((||.t.|| * ||.s.||) ") by XCMPLX_0:def 9
.= ||.(((||.t.|| * ||.s.||) ") * (g . (t,s))).|| by A11, NORMSP_1:def 1
.= ||.(((||.t.|| ") * (||.s.|| ")) * (g . (t,s))).|| by XCMPLX_1:204
.= ||.((||.t.|| ") * ((||.s.|| ") * (g . (t,s)))).|| by RLVECT_1:def 7
.= ||.((||.t.|| ") * (g . (t,s1))).|| by LOPBAN_8:12
.= ||.(g . (t1,s1)).|| by LOPBAN_8:12 ;
then ||.(g . (t,s)).|| / (||.t.|| * ||.s.||) <= K by A1, A13, SEQ_4:def 1;
hence ||.(g . (t,s)).|| <= K * (||.t.|| * ||.s.||) by A8, XREAL_1:64; :: thesis: verum

end;

end;

end;

hence ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.|| ; :: thesis: verum

end;

take K = K; :: thesis: g is Lipschitzian
0 <= K

proof

consider r0 being object such that
A14: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 = r0 as Real by A14;

now :: thesis: for r being Real st r in PreNorms g holds
0 <= r

let r be Real; :: thesis: ( r in PreNorms g implies 0 <= r )
assume r in PreNorms g ; :: thesis: 0 <= r
then ex t being VECTOR of X ex s being VECTOR of Y st
( r = ||.(g . (t,s)).|| & ||.t.|| <= 1 & ||.s.|| <= 1 ) ;
hence 0 <= r ; :: thesis: verum

end;

then 0 <= r0 by A14;
hence 0 <= K by A1, A14, SEQ_4:def 1; :: thesis: verum

end;

hence g is Lipschitzian by A2; :: thesis: verum

end;

hence ( g is Lipschitzian iff PreNorms g is bounded_above ) ; :: thesis: verum