let X be RealUnitarySpace; :: thesis: for f being linear-Functional of X
for g being linear-Functional of (RUSp2RNSp X) 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 (RUSp2RNSp X) st f = g holds
( f is Lipschitzian iff g is Lipschitzian )
let g be linear-Functional of (RUSp2RNSp X); :: 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 * ||.x.|| ) ) by BHSP_6:def 4;
for y being Point of (RUSp2RNSp X) holds |.(g . y).| <= K * ||.y.||

proof

let y be Point of (RUSp2RNSp X); :: thesis: |.(g . y).| <= K * ||.y.||
reconsider x = y as Point of X ;
||.y.|| = ||.x.|| by Def1;
hence |.(g . y).| <= K * ||.y.|| 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 (RUSp2RNSp X) holds |.(g . y).| <= K * ||.y.|| ) ) ;
A4: K + 0 < K + 1 by XREAL_1:8;
for x being Point of X holds |.(f . x).| <= (K + 1) * ||.x.||

proof

let x be Point of X; :: thesis: |.(f . x).| <= (K + 1) * ||.x.||
reconsider y = x as Point of (RUSp2RNSp X) ;
||.x.|| = ||.y.|| by Def1;
then B3: |.(f . x).| <= K * ||.x.|| by A2, AS;
0 <= ||.x.|| by BHSP_1:28;
then K * ||.x.|| <= (K + 1) * ||.x.|| by A4, XREAL_1:64;
hence |.(f . x).| <= (K + 1) * ||.x.|| by B3, XXREAL_0:2; :: thesis: verum

end;

hence f is Lipschitzian by A2, BHSP_6:def 4; :: thesis: verum