let X be RealUnitarySpace; :: thesis: for f being Point of ()
for g being Lipschitzian linear-Functional of X st g = f holds
for t being VECTOR of X holds |.(g . t).| <= *

let f be Point of (); :: thesis: for g being Lipschitzian linear-Functional of X st g = f holds
for t being VECTOR of X holds |.(g . t).| <= *

let g be Lipschitzian linear-Functional of X; :: thesis: ( g = f implies for t being VECTOR of X holds |.(g . t).| <= * )
assume A1: g = f ; :: thesis: for t being VECTOR of X holds |.(g . t).| <= *
let t be VECTOR of X; :: thesis: |.(g . t).| <= *
per cases ( t = 0. X or t <> 0. X ) ;
suppose A3: t = 0. X ; :: thesis: |.(g . t).| <= *
then A4: ||.t.|| = 0 by BHSP_1:26;
g . t = g . (0 * (0. X)) by A3
.= 0 * (g . (0. X)) by HAHNBAN:def 3
.= 0 ;
hence |.(g . t).| <= * by ; :: thesis: verum
end;
suppose A5: t <> 0. X ; :: thesis: |.(g . t).| <= *
reconsider t1 = () * t as VECTOR of X ;
A6: ||.t.|| <> 0 by ;
then B61: 0 < by BHSP_1:28;
A7: |.().| = |.(1 * ()).|
.= |.(1 / ).| by XCMPLX_0:def 9
.= 1 / by
.= 1 * () by XCMPLX_0:def 9
.= " ;
A8: |.(g . t).| / = |.(g . t).| * () by XCMPLX_0:def 9
.= |.(() * (g . t)).| by
.= |.(g . t1).| by HAHNBAN:def 3 ;
||.t1.|| = |.().| * by BHSP_1:27
.= 1 by ;
then |.(g . t).| / in { |.(g . s).| where s is VECTOR of X : <= 1 } by A8;
then |.(g . t).| / <= upper_bound () by SEQ_4:def 1;
then A9: |.(g . t).| / <= by ;
A10: (|.(g . t).| / ) * = (|.(g . t).| * ()) * by XCMPLX_0:def 9
.= |.(g . t).| * (() * )
.= |.(g . t).| * 1 by
.= |.(g . t).| ;
0 <= by BHSP_1:28;
hence |.(g . t).| <= * by ; :: thesis: verum
end;
end;