deffunc H₁( Element of (DualSp X)) -> Element of REAL = $1 . x;
P0: ex f being Function of the carrier of (DualSp X),REAL st
for fai being Element of (DualSp X) holds f . fai = H₁(fai) from FUNCT_2:sch 4();
consider f being Function of the carrier of (DualSp X),REAL such that
P1: for fai being Point of (DualSp X) holds f . fai = fai . x by P0;
P2: f is additive

proof

let y, z be Point of (DualSp X); :: according to HAHNBAN:def 2 :: thesis: f . (y + z) = (f . y) + (f . z)
f . (y + z) = (y + z) . x by P1
.= (y . x) + (z . x) by DUALSP01:29
.= (f . y) + (z . x) by P1 ;
hence f . (y + z) = (f . y) + (f . z) by P1; :: thesis: verum

end;

P3: f is homogeneous

proof

let y be Point of (DualSp X); :: according to HAHNBAN:def 3 :: thesis: for b₁ being object holds f . (b₁ * y) = b₁ * (f . y)
let r be Real; :: thesis: f . (r * y) = r * (f . y)
f . (r * y) = (r * y) . x by P1
.= r * (y . x) by DUALSP01:30 ;
hence f . (r * y) = r * (f . y) by P1; :: thesis: verum

end;

for y being Point of (DualSp X) holds |.(f . y).| <= ||.x.|| * ||.y.||

proof

let y be Point of (DualSp X); :: thesis: |.(f . y).| <= ||.x.|| * ||.y.||
reconsider y1 = y as Lipschitzian linear-Functional of X by DUALSP01:def 10;
|.(y1 . x).| <= ||.y.|| * ||.x.|| by DUALSP01:26;
hence |.(f . y).| <= ||.x.|| * ||.y.|| by P1; :: thesis: verum

end;

then f is Lipschitzian ;
then reconsider f = f as Point of (DualSp (DualSp X)) by P2, P3, DUALSP01:def 10;
take f ; :: thesis: for f being Point of (DualSp X) holds f . f = f . x
thus for f being Point of (DualSp X) holds f . f = f . x by P1; :: thesis: verum