reconsider f = BidualFunc X as Function of X,(DualSp (DualSp X)) ;
A0: ( f is additive & f is homogeneous ) ;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A1: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then reconsider y1 = x1, y2 = x2 as Point of X ;
A3: f . (y1 - y2) = BiDual (y1 - y2) by Def2;
y1 - y2 = y1 + ((- 1) * y2) by RLVECT_1:16;
then A5: f . (y1 - y2) = (f . y1) + (f . ((- 1) * y2)) by A0;
f . ((- 1) * y2) = (- 1) * (f . y2) by LOPBAN_1:def 5;
then f . (y1 - y2) = (f . y1) - (f . y2) by A5, RLVECT_1:16;
then A7: BiDual (y1 - y2) = 0. (DualSp (DualSp X)) by A3, A1, RLVECT_1:15;
for g being Lipschitzian linear-Functional of X holds g . (y1 - y2) = 0

proof

let g be Lipschitzian linear-Functional of X; :: thesis: g . (y1 - y2) = 0
reconsider g1 = g as Point of (DualSp X) by DUALSP01:def 10;
A8: (BiDual (y1 - y2)) . g1 = g1 . (y1 - y2) by Def1;
the carrier of (DualSp X) --> 0 = 0. (DualSp (DualSp X)) by DUALSP01:25;
hence g . (y1 - y2) = 0 by A7, A8, FUNCOP_1:7; :: thesis: verum

end;

then y1 - y2 = 0. X by Lm72;
hence x1 = x2 by RLVECT_1:21; :: thesis: verum

end;

hence BidualFunc X is one-to-one ; :: thesis: verum