let X, Y be RealNormSpace; :: thesis: for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y)
for g being bounded LinearOperator of X,Y st g = f holds
for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||
let f be Point of (R_NormSpace_of_BoundedLinearOperators X,Y); :: thesis: for g being bounded LinearOperator of X,Y st g = f holds
for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||
let g be bounded LinearOperator of X,Y; :: thesis: ( g = f implies for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.|| )
assume A1: g = f ; :: thesis: for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||
A2: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th32;

now

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

now

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

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

then A4: g . t = g . (0 * (0. X)) by RLVECT_1:23
.= 0 * (g . (0. X)) by Def6
.= 0. Y by RLVECT_1:23 ;
||.t.|| = 0 by A3;
hence ||.(g . t).|| <= ||.f.|| * ||.t.|| by A4; :: thesis: verum

end;

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

then A5: ||.t.|| <> 0 by NORMSP_1:def 2;
then A6: ||.t.|| > 0 by NORMSP_1:8;
A7: abs (||.t.|| " ) = abs (1 * (||.t.|| " ))
.= abs (1 / ||.t.||) by XCMPLX_0:def 9
.= 1 / (abs ||.t.||) by ABSVALUE:15
.= 1 / ||.t.|| by A6, ABSVALUE:def 1
.= 1 * (||.t.|| " ) by XCMPLX_0:def 9
.= ||.t.|| " ;
reconsider t1 = (||.t.|| " ) * t as VECTOR of X ;
A8: ||.t1.|| = (abs (||.t.|| " )) * ||.t.|| by NORMSP_1:def 2
.= 1 by A5, A7, XCMPLX_0:def 7 ;
||.(g . t).|| / ||.t.|| = ||.(g . t).|| * (||.t.|| " ) by XCMPLX_0:def 9
.= ||.((||.t.|| " ) * (g . t)).|| by A7, NORMSP_1:def 2
.= ||.(g . t1).|| by Def6 ;
then ||.(g . t).|| / ||.t.|| in { ||.(g . s).|| where s is VECTOR of X : ||.s.|| <= 1 } by A8;
then ||.(g . t).|| / ||.t.|| <= sup (PreNorms g) by A2, SEQ_4:def 4;
then ||.(g . t).|| / ||.t.|| <= (BoundedLinearOperatorsNorm X,Y) . g by Th36;
then A9: ||.(g . t).|| / ||.t.|| <= ||.f.|| by A1, NORMSP_1:def 1;
(||.(g . t).|| / ||.t.||) * ||.t.|| = (||.(g . t).|| * (||.t.|| " )) * ||.t.|| by XCMPLX_0:def 9
.= ||.(g . t).|| * ((||.t.|| " ) * ||.t.||)
.= ||.(g . t).|| * 1 by A5, XCMPLX_0:def 7
.= ||.(g . t).|| ;
hence ||.(g . t).|| <= ||.f.|| * ||.t.|| by A6, A9, XREAL_1:66; :: thesis: verum

end;

end;

end;

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

end;

hence for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.|| ; :: thesis: verum