let X be RealUnitarySpace; :: thesis: for f being linear-Functional of X
for g being linear-Functional of () st f = g holds
( f is Lipschitzian iff g is Lipschitzian )

let f be linear-Functional of X; :: thesis: for g being linear-Functional of () st f = g holds
( f is Lipschitzian iff g is Lipschitzian )

let g be linear-Functional of (); :: thesis: ( f = g implies ( f is Lipschitzian iff g is Lipschitzian ) )
assume AS: f = g ; :: thesis: ( f is Lipschitzian iff g is Lipschitzian )
set Y = RUSp2RNSp X;
hereby :: thesis: ( g is Lipschitzian implies f is Lipschitzian )
assume f is Lipschitzian ; :: thesis: g is Lipschitzian
then consider K being Real such that
A1: ( 0 < K & ( for x being Point of X holds |.(f . x).| <= K * ) ) by BHSP_6:def 4;
for y being Point of () holds |.(g . y).| <= K *
proof
let y be Point of (); :: thesis: |.(g . y).| <= K *
reconsider x = y as Point of X ;
||.y.|| = by Def1;
hence |.(g . y).| <= K * by A1, AS; :: thesis: verum
end;
hence g is Lipschitzian by A1; :: thesis: verum
end;
assume g is Lipschitzian ; :: thesis: f is Lipschitzian
then consider K being Real such that
A2: ( 0 <= K & ( for y being Point of () holds |.(g . y).| <= K * ) ) ;
A4: K + 0 < K + 1 by XREAL_1:8;
for x being Point of X holds |.(f . x).| <= (K + 1) *
proof
let x be Point of X; :: thesis: |.(f . x).| <= (K + 1) *
reconsider y = x as Point of () ;
||.x.|| = by Def1;
then B3: |.(f . x).| <= K * by A2, AS;
0 <= by BHSP_1:28;
then K * <= (K + 1) * by ;
hence |.(f . x).| <= (K + 1) * by ; :: thesis: verum
end;
hence f is Lipschitzian by ; :: thesis: verum