let X be RealNormSpace; :: thesis: for Y being SubRealNormSpace of X
for L being Lipschitzian linear-Functional of X holds L | the carrier of Y is Lipschitzian linear-Functional of Y
let Y be SubRealNormSpace of X; :: thesis: for L being Lipschitzian linear-Functional of X holds L | the carrier of Y is Lipschitzian linear-Functional of Y
let L be Lipschitzian linear-Functional of X; :: thesis: L | the carrier of Y is Lipschitzian linear-Functional of Y
set Y1 = the carrier of Y;
A1: the carrier of Y c= the carrier of X by DUALSP01:def 16;
then reconsider L1 = L | the carrier of Y as Functional of Y by FUNCT_2:32;
A2: L1 is additive

proof

let x, y be Point of Y; :: according to HAHNBAN:def 2 :: thesis: L1 . (x + y) = K55((L1 . x),(L1 . y))
reconsider x1 = x, y1 = y as Point of X by A1;
thus L1 . (x + y) = L . (x + y) by FUNCT_1:49
.= L . (x1 + y1) by NORMSP_3:28
.= (L . x1) + (L . y1) by HAHNBAN:def 2
.= (L1 . x) + (L . y) by FUNCT_1:49
.= (L1 . x) + (L1 . y) by FUNCT_1:49 ; :: thesis: verum

end;

A3: L1 is homogeneous

proof

let x be Point of Y; :: according to HAHNBAN:def 3 :: thesis: for b₁ being object holds L1 . (b₁ * x) = b₁ * (L1 . x)
let r be Real; :: thesis: L1 . (r * x) = r * (L1 . x)
reconsider x1 = x as Point of X by A1;
thus L1 . (r * x) = L . (r * x) by FUNCT_1:49
.= L . (r * x1) by NORMSP_3:28
.= r * (L . x1) by HAHNBAN:def 3
.= r * (L1 . x) by FUNCT_1:49 ; :: thesis: verum

end;

consider K being Real such that
A4: ( 0 <= K & ( for x being Point of X holds |.(L . x).| <= K * ||.x.|| ) ) by DUALSP01:def 9;
for x being Point of Y holds |.(L1 . x).| <= K * ||.x.||

proof

let x be Point of Y; :: thesis: |.(L1 . x).| <= K * ||.x.||
reconsider x1 = x as Point of X by A1;
|.(L . x1).| <= K * ||.x1.|| by A4;
then |.(L . x1).| <= K * ||.x.|| by NORMSP_3:28;
hence |.(L1 . x).| <= K * ||.x.|| by FUNCT_1:49; :: thesis: verum

end;

then L1 is Lipschitzian by A4;
hence L | the carrier of Y is Lipschitzian linear-Functional of Y by A2, A3; :: thesis: verum