let X be RealNormSpace; :: thesis: for x being object holds
( x is additive homogeneous Lipschitzian Function of X,REAL iff x is additive homogeneous Lipschitzian Function of X,RNS_Real )
let x be object ; :: thesis: ( x is additive homogeneous Lipschitzian Function of X,REAL iff x is additive homogeneous Lipschitzian Function of X,RNS_Real )

hereby :: thesis: ( x is additive homogeneous Lipschitzian Function of X,RNS_Real implies x is additive homogeneous Lipschitzian Function of X,REAL )

assume A1: x is additive homogeneous Lipschitzian Function of X,REAL ; :: thesis: x is additive homogeneous Lipschitzian Function of X,RNS_Real
then reconsider f = x as Lipschitzian linear-Functional of X ;
reconsider g = x as additive homogeneous Function of X,RNS_Real by A1, LMN6;
consider K being Real such that
X1: ( 0 <= K & ( for v being VECTOR of X holds |.(f . v).| <= K * ||.v.|| ) ) by DUALSP01:def 9;
for v being VECTOR of X holds ||.(g . v).|| <= K * ||.v.||

proof

let v be VECTOR of X; :: thesis: ||.(g . v).|| <= K * ||.v.||
|.(f . v).| <= K * ||.v.|| by X1;
hence ||.(g . v).|| <= K * ||.v.|| by EUCLID:def 2; :: thesis: verum

end;

hence x is additive homogeneous Lipschitzian Function of X,RNS_Real by X1, LOPBAN_1:def 8; :: thesis: verum

end;

assume B1: x is additive homogeneous Lipschitzian Function of X,RNS_Real ; :: thesis: x is additive homogeneous Lipschitzian Function of X,REAL
then reconsider g = x as additive homogeneous Lipschitzian Function of X,RNS_Real ;
reconsider f = x as additive homogeneous Function of X,REAL by LMN6, B1;
consider K being Real such that
X1: ( 0 <= K & ( for v being VECTOR of X holds ||.(g . v).|| <= K * ||.v.|| ) ) by LOPBAN_1:def 8;
for v being VECTOR of X holds |.(f . v).| <= K * ||.v.||

proof

let v be VECTOR of X; :: thesis: |.(f . v).| <= K * ||.v.||
||.(g . v).|| <= K * ||.v.|| by X1;
hence |.(f . v).| <= K * ||.v.|| by EUCLID:def 2; :: thesis: verum

end;

then ( f is Lipschitzian & f is additive & f is homogeneous ) by X1;
hence x is additive homogeneous Lipschitzian Function of X,REAL ; :: thesis: verum