given g1, g2 being Point of X such that A2: for f being Lipschitzian linear-Functional of X holds
( f * x is convergent & lim (f * x) = f . g1 ) and
A3: for f being Lipschitzian linear-Functional of X holds
( f * x is convergent & lim (f * x) = f . g2 ) and
A4: g1 <> g2 ; :: thesis: contradiction
now :: thesis: for f being Lipschitzian linear-Functional of X holds f . (g1 - g2) = 0
let f be Lipschitzian linear-Functional of X; :: thesis: f . (g1 - g2) = 0
f . (g1 - g2) = (f . g1) - (f . g2) by HAHNBAN:19
.= (lim (f * x)) - (f . g2) by A2
.= (lim (f * x)) - (lim (f * x)) by A3 ;
hence f . (g1 - g2) = 0 ; :: thesis: verum
end;
then g1 - g2 = 0. X by DUALSP02:8;
hence contradiction by A4, RLVECT_1:21; :: thesis: verum