let X, Y be ComplexNormSpace; :: thesis: for g being LinearOperator of X,Y holds
( g is bounded iff PreNorms g is bounded_above )
let g be LinearOperator of X,Y; :: thesis: ( g is bounded iff PreNorms g is bounded_above )

now

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

proof

A3: now

let r be Real; :: thesis: ( r in PreNorms g implies 0 <= r )
assume A4: r in PreNorms g ; :: thesis: 0 <= r
consider t being VECTOR of X such that
A5: ( r = ||.(g . t).|| & ||.t.|| <= 1 ) by A4;
thus 0 <= r by A5, CLVECT_1:106; :: thesis: verum

end;

consider r0 being set such that
A6: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 = r0 as Real by A6;
0 <= r0 by A3, A6;
hence 0 <= K by A1, A6, SEQ_4:def 4; :: thesis: verum

end;

A7: now

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

now

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

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

then A9: g . t = g . (0c * (0. X)) by CLVECT_1:2
.= 0c * (g . (0. X)) by Def4
.= 0. Y by CLVECT_1:2 ;
||.t.|| = 0 by A8, CLVECT_1:def 11;
hence ||.(g . t).|| <= K * ||.t.|| by A9, CLVECT_1:def 11; :: thesis: verum

end;

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

then A10: ||.t.|| <> 0 by CLVECT_1:def 11;
then A11: ||.t.|| > 0 by CLVECT_1:106;
A12: |.((||.t.|| " ) + (0 * <i> )).| = abs (1 * (||.t.|| " ))
.= abs (1 / ||.t.||) by XCMPLX_0:def 9
.= 1 / (abs ||.t.||) by ABSVALUE:15
.= 1 / ||.t.|| by A11, ABSVALUE:def 1
.= 1 * (||.t.|| " ) by XCMPLX_0:def 9
.= ||.t.|| " ;
reconsider t0 = (||.t.|| " ) + (0 * <i> ) as Element of COMPLEX by XCMPLX_0:def 2;
reconsider t1 = t0 * t as VECTOR of X ;
A13: ||.t1.|| = |.t0.| * ||.t.|| by CLVECT_1:def 11
.= 1 by A10, A12, XCMPLX_0:def 7 ;
||.(g . t).|| / ||.t.|| = ||.(g . t).|| * |.t0.| by A12, XCMPLX_0:def 9
.= ||.(t0 * (g . t)).|| by CLVECT_1:def 11
.= ||.(g . t1).|| by Def4 ;
then ||.(g . t).|| / ||.t.|| in PreNorms g by A13;
then A14: ||.(g . t).|| / ||.t.|| <= K by A1, SEQ_4:def 4;
(||.(g . t).|| / ||.t.||) * ||.t.|| = (||.(g . t).|| * (||.t.|| " )) * ||.t.|| by XCMPLX_0:def 9
.= ||.(g . t).|| * ((||.t.|| " ) * ||.t.||)
.= ||.(g . t).|| * 1 by A10, XCMPLX_0:def 7
.= ||.(g . t).|| ;
hence ||.(g . t).|| <= K * ||.t.|| by A11, A14, XREAL_1:66; :: thesis: verum

end;

end;

end;

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

end;

take K = K; :: thesis: g is bounded
thus g is bounded by A2, A7, Def7; :: thesis: verum

end;

hence ( g is bounded iff PreNorms g is bounded_above ) by Th30; :: thesis: verum