let X, Y be RealNormSpace; :: thesis: for g being LinearOperator of X,Y holds
( g is Lipschitzian iff PreNorms g is bounded_above )
let g be LinearOperator of X,Y; :: 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 holds ||.(g . t).|| <= K * ||.t.||

let t be VECTOR of X; :: thesis: ||.(g . t).|| <= K * ||.t.||

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

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

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

then A4: ||.t.|| = 0 ;
g . t = g . (0 * (0. X)) by A3
.= 0 * (g . (0. X)) by Def5
.= 0. Y by RLVECT_1:10 ;
hence ||.(g . t).|| <= K * ||.t.|| by A4; :: thesis: verum

end;

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

reconsider t1 = (||.t.|| ") * t as VECTOR of X ;
A6: ||.t.|| <> 0 by A5, NORMSP_0:def 5;
A7: (||.(g . t).|| / ||.t.||) * ||.t.|| = (||.(g . t).|| * (||.t.|| ")) * ||.t.|| by XCMPLX_0:def 9
.= ||.(g . t).|| * ((||.t.|| ") * ||.t.||)
.= ||.(g . t).|| * 1 by A6, XCMPLX_0:def 7
.= ||.(g . t).|| ;
A8: |.(||.t.|| ").| = |.(1 * (||.t.|| ")).|
.= |.(1 / ||.t.||).| by XCMPLX_0:def 9
.= 1 / |.||.t.||.| by ABSVALUE:7
.= 1 / ||.t.|| by ABSVALUE:def 1
.= 1 * (||.t.|| ") by XCMPLX_0:def 9
.= ||.t.|| " ;
||.t1.|| = |.(||.t.|| ").| * ||.t.|| by NORMSP_1:def 1
.= 1 by A6, A8, XCMPLX_0:def 7 ;
then A9: ||.(g . t1).|| in { ||.(g . s).|| where s is VECTOR of X : ||.s.|| <= 1 } ;
||.(g . t).|| / ||.t.|| = ||.(g . t).|| * (||.t.|| ") by XCMPLX_0:def 9
.= ||.((||.t.|| ") * (g . t)).|| by A8, NORMSP_1:def 1
.= ||.(g . t1).|| by Def5 ;
then ||.(g . t).|| / ||.t.|| <= K by A1, A9, SEQ_4:def 1;
hence ||.(g . t).|| <= K * ||.t.|| by A7, XREAL_1:64; :: thesis: verum

end;

end;

end;

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

end;

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

proof

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

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 st
( r = ||.(g . t).|| & ||.t.|| <= 1 ) ;
hence 0 <= r ; :: thesis: verum

end;

then 0 <= r0 by A10;
hence 0 <= K by A1, A10, 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 ) by Th27; :: thesis: verum