let X, Y be ComplexNormSpace; :: 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 () 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 *
let t be VECTOR of X; :: thesis: ||.(g . t).|| <= K *
now :: thesis: ( ( t = 0. X & ||.(g . t).|| <= K * ) or ( t <> 0. X & ||.(g . t).|| <= K * ) )
per cases ( t = 0. X or t <> 0. X ) ;
case A3: t = 0. X ; :: thesis: ||.(g . t).|| <= K *
then A4: ||.t.|| = 0 by NORMSP_0:def 6;
g . t = g . (0c * (0. X)) by
.= 0c * (g . (0. X)) by Def3
.= 0. Y by CLVECT_1:1 ;
hence ||.(g . t).|| <= K * by ; :: thesis: verum
end;
case A5: t <> 0. X ; :: thesis: ||.(g . t).|| <= K *
reconsider t0 = () + () as Element of COMPLEX by XCMPLX_0:def 2;
reconsider t1 = t0 * t as VECTOR of X ;
A6: ||.t.|| <> 0 by ;
then A7: ||.t.|| > 0 by CLVECT_1:105;
A8: |.(() + ()).| = |.(1 * ()).|
.= |.(1 / ).| by XCMPLX_0:def 9
.= 1 / by ABSVALUE:7
.= 1 / by
.= 1 * () by XCMPLX_0:def 9
.= " ;
then A9: ||.(g . t).|| / = ||.(g . t).|| * |.t0.| by XCMPLX_0:def 9
.= ||.(t0 * (g . t)).|| by CLVECT_1:def 13
.= ||.(g . t1).|| by Def3 ;
||.t1.|| = |.t0.| * by CLVECT_1:def 13
.= 1 by ;
then ||.(g . t).|| / in PreNorms g by A9;
then A10: ||.(g . t).|| / <= K by ;
(||.(g . t).|| / ) * = (||.(g . t).|| * ()) * by XCMPLX_0:def 9
.= ||.(g . t).|| * (() * )
.= ||.(g . t).|| * 1 by
.= ||.(g . t).|| ;
hence ||.(g . t).|| <= K * by ; :: thesis: verum
end;
end;
end;
hence ||.(g . t).|| <= K * ; :: thesis: verum
end;
take K = K; :: thesis: g is Lipschitzian
0 <= K
proof
consider r0 being object such that
A11: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 = r0 as Real by A11;
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).|| & <= 1 ) ;
hence 0 <= r by CLVECT_1:105; :: thesis: verum
end;
then 0 <= r0 by A11;
hence 0 <= K by ; :: thesis: verum
end;
hence g is Lipschitzian by A2; :: thesis: verum
end;
hence ( g is Lipschitzian iff PreNorms g is bounded_above ) by Th26; :: thesis: verum