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

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.||

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

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

A3:
L1 is homogeneous
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;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

proof

consider K being Real such that
let x be Point of Y; :: according to HAHNBAN:def 3 :: thesis: for b_{1} being object holds L1 . (b_{1} * x) = b_{1} * (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;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

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

then
L1 is Lipschitzian
by A4;
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;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

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