let X be RealNormSpace; :: thesis: for x being sequence of X st X is Reflexive holds
( x is weakly-convergent iff (BidualFunc X) * x is weakly*-convergent )
let x be sequence of X; :: thesis: ( X is Reflexive implies ( x is weakly-convergent iff (BidualFunc X) * x is weakly*-convergent ) )
assume AS: X is Reflexive ; :: thesis: ( x is weakly-convergent iff (BidualFunc X) * x is weakly*-convergent )
set f = (BidualFunc X) * x;

hereby :: thesis: ( (BidualFunc X) * x is weakly*-convergent implies x is weakly-convergent )

assume AS: x is weakly-convergent ; :: thesis: (BidualFunc X) * x is weakly*-convergent
reconsider x0 = w-lim x as Point of X ;
for g being Point of (DualSp X) holds
( ((BidualFunc X) * x) # g is convergent & lim (((BidualFunc X) * x) # g) = (BiDual x0) . g )

proof

let g be Point of (DualSp X); :: thesis: ( ((BidualFunc X) * x) # g is convergent & lim (((BidualFunc X) * x) # g) = (BiDual x0) . g )
reconsider f0 = BiDual x0 as Point of (DualSp (DualSp X)) ;
A3: for n being Nat holds (((BidualFunc X) * x) # g) . n = (g * x) . n

proof

let n be Nat; :: thesis: (((BidualFunc X) * x) # g) . n = (g * x) . n
reconsider f1 = BiDual (x . n) as Point of (DualSp (DualSp X)) ;
((BidualFunc X) * x) . n = (BidualFunc X) . (x . n) by FUNCT_2:15, ORDINAL1:def 12;
then B2: ((BidualFunc X) * x) . n = BiDual (x . n) by DUALSP02:def 2;
(((BidualFunc X) * x) # g) . n = (((BidualFunc X) * x) . n) . g by Def1;
then (((BidualFunc X) * x) # g) . n = g . (x . n) by B2, DUALSP02:def 1;
hence (((BidualFunc X) * x) # g) . n = (g * x) . n by FUNCT_2:15, ORDINAL1:def 12; :: thesis: verum

end;

reconsider g1 = g as Lipschitzian linear-Functional of X by DUALSP01:def 10;
A41: ( g1 * x is convergent & lim (g1 * x) = g1 . x0 ) by DefWeaklim, AS;
A5: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
|.(((((BidualFunc X) * x) # g) . n) - (f0 . g)).| < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
|.(((((BidualFunc X) * x) # g) . n) - (f0 . g)).| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
|.(((((BidualFunc X) * x) # g) . n) - (f0 . g)).| < r
then consider m being Nat such that
B1: for n being Nat st m <= n holds
|.(((g1 * x) . n) - (g1 . x0)).| < r by A41, SEQ_2:def 7;
take m ; :: thesis: for n being Nat st m <= n holds
|.(((((BidualFunc X) * x) # g) . n) - (f0 . g)).| < r
thus for n being Nat st m <= n holds
|.(((((BidualFunc X) * x) # g) . n) - (f0 . g)).| < r :: thesis: verum

proof

let n be Nat; :: thesis: ( m <= n implies |.(((((BidualFunc X) * x) # g) . n) - (f0 . g)).| < r )
assume C3: m <= n ; :: thesis: |.(((((BidualFunc X) * x) # g) . n) - (f0 . g)).| < r
f0 . g = g . x0 by DUALSP02:def 1;
then |.(((((BidualFunc X) * x) # g) . n) - (f0 . g)).| = |.(((g1 * x) . n) - (g1 . x0)).| by A3;
hence |.(((((BidualFunc X) * x) # g) . n) - (f0 . g)).| < r by B1, C3; :: thesis: verum

end;

end;

then ((BidualFunc X) * x) # g is convergent ;
hence ( ((BidualFunc X) * x) # g is convergent & lim (((BidualFunc X) * x) # g) = (BiDual x0) . g ) by A5, SEQ_2:def 7; :: thesis: verum

end;

hence (BidualFunc X) * x is weakly*-convergent ; :: thesis: verum

end;

assume (BidualFunc X) * x is weakly*-convergent ; :: thesis: x is weakly-convergent
then consider f0 being Point of (DualSp (DualSp X)) such that
A0: for h being Point of (DualSp X) holds
( ((BidualFunc X) * x) # h is convergent & lim (((BidualFunc X) * x) # h) = f0 . h ) ;
consider x0 being Point of X such that
A1: for g being Point of (DualSp X) holds f0 . g = g . x0 by AS, DUALSP02:21;
for g being Lipschitzian linear-Functional of X holds
( g * x is convergent & lim (g * x) = g . x0 )

proof

let g be Lipschitzian linear-Functional of X; :: thesis: ( g * x is convergent & lim (g * x) = g . x0 )
reconsider g1 = g as Point of (DualSp X) by DUALSP01:def 10;
A3: for n being Nat holds (g * x) . n = (((BidualFunc X) * x) # g1) . n

proof

let n be Nat; :: thesis: (g * x) . n = (((BidualFunc X) * x) # g1) . n
reconsider f1 = BiDual (x . n) as Point of (DualSp (DualSp X)) ;
B2: ((BidualFunc X) * x) . n = (BidualFunc X) . (x . n) by FUNCT_2:15, ORDINAL1:def 12
.= BiDual (x . n) by DUALSP02:def 2 ;
thus (g * x) . n = g1 . (x . n) by FUNCT_2:15, ORDINAL1:def 12
.= f1 . g1 by DUALSP02:def 1
.= (((BidualFunc X) * x) # g1) . n by B2, Def1 ; :: thesis: verum

end;

B4: ( ((BidualFunc X) * x) # g1 is convergent & lim (((BidualFunc X) * x) # g1) = f0 . g1 ) by A0;
A5: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
|.(((g * x) . n) - (g1 . x0)).| < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
|.(((g * x) . n) - (g1 . x0)).| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
|.(((g * x) . n) - (g1 . x0)).| < r
then consider m being Nat such that
B1: for n being Nat st m <= n holds
|.(((((BidualFunc X) * x) # g1) . n) - (f0 . g1)).| < r by SEQ_2:def 7, B4;
take m ; :: thesis: for n being Nat st m <= n holds
|.(((g * x) . n) - (g1 . x0)).| < r

hereby :: thesis: verum

let n be Nat; :: thesis: ( m <= n implies |.(((g * x) . n) - (g1 . x0)).| < r )
assume C3: m <= n ; :: thesis: |.(((g * x) . n) - (g1 . x0)).| < r
f0 . g1 = g1 . x0 by A1;
then |.(((g * x) . n) - (g1 . x0)).| = |.(((((BidualFunc X) * x) # g1) . n) - (f0 . g1)).| by A3;
hence |.(((g * x) . n) - (g1 . x0)).| < r by B1, C3; :: thesis: verum

end;

end;

then g * x is convergent ;
hence ( g * x is convergent & lim (g * x) = g . x0 ) by A5, SEQ_2:def 7; :: thesis: verum

end;

hence x is weakly-convergent ; :: thesis: verum