let X be RealNormSpace; :: thesis: ( not X is trivial & X is Reflexive implies X is RealBanachSpace )
assume AS: ( not X is trivial & X is Reflexive ) ; :: thesis: X is RealBanachSpace
then P1: BidualFunc X is onto ;
for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds
seq is convergent

proof

let seq be sequence of X; :: thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )
assume P2: seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent
reconsider seq1 = (BidualFunc X) * seq as sequence of (DualSp (DualSp X)) ;
XX: ( BidualFunc X is additive & BidualFunc X is homogeneous ) ;
for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r

proof

let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r
then consider k being Nat such that
A1: for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r by P2, RSSPACE3:8;
AK: for n, m being Nat st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r

proof

let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((seq1 . n) - (seq1 . m)).|| < r )
assume ( n >= k & m >= k ) ; :: thesis: ||.((seq1 . n) - (seq1 . m)).|| < r
then A2: ||.((seq . n) - (seq . m)).|| < r by A1;
( n in NAT & m in NAT ) by ORDINAL1:def 12;
then ( n in dom seq & m in dom seq ) by FUNCT_2:def 1;
then A4: ( seq1 . n = (BidualFunc X) . (seq . n) & seq1 . m = (BidualFunc X) . (seq . m) ) by FUNCT_1:13;
(seq . n) - (seq . m) = (seq . n) + ((- 1) * (seq . m)) by RLVECT_1:16;
then A7: (BidualFunc X) . ((seq . n) - (seq . m)) = ((BidualFunc X) . (seq . n)) + ((BidualFunc X) . ((- 1) * (seq . m))) by XX;
(BidualFunc X) . ((- 1) * (seq . m)) = (- 1) * ((BidualFunc X) . (seq . m)) by LOPBAN_1:def 5;
then (BidualFunc X) . ((seq . n) - (seq . m)) = ((BidualFunc X) . (seq . n)) - ((BidualFunc X) . (seq . m)) by A7, RLVECT_1:16;
hence ||.((seq1 . n) - (seq1 . m)).|| < r by A2, AS, A4, LMNORM; :: thesis: verum

end;

take k ; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r
thus for n, m being Nat st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r by AK; :: thesis: verum

end;

then P5: seq1 is convergent by LOPBAN_1:def 15, RSSPACE3:8;
consider s being Point of X such that
P7: lim seq1 = (BidualFunc X) . s by P1, FUNCT_2:113;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - s).|| < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - s).|| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - s).|| < r
then consider m being Nat such that
B1: for n being Nat st m <= n holds
||.((seq1 . n) - (lim seq1)).|| < r by P5, NORMSP_1:def 7;
BK: for n being Nat st m <= n holds
||.((seq . n) - s).|| < r

proof

let n be Nat; :: thesis: ( m <= n implies ||.((seq . n) - s).|| < r )
assume m <= n ; :: thesis: ||.((seq . n) - s).|| < r
then B2: ||.((seq1 . n) - (lim seq1)).|| < r by B1;
n in NAT by ORDINAL1:def 12;
then n in dom seq by FUNCT_2:def 1;
then B4: seq1 . n = (BidualFunc X) . (seq . n) by FUNCT_1:13;
(seq . n) - s = (seq . n) + ((- 1) * s) by RLVECT_1:16;
then B6: (BidualFunc X) . ((seq . n) - s) = ((BidualFunc X) . (seq . n)) + ((BidualFunc X) . ((- 1) * s)) by XX;
(BidualFunc X) . ((- 1) * s) = (- 1) * ((BidualFunc X) . s) by LOPBAN_1:def 5;
then (BidualFunc X) . ((seq . n) - s) = ((BidualFunc X) . (seq . n)) - ((BidualFunc X) . s) by B6, RLVECT_1:16;
hence ||.((seq . n) - s).|| < r by B2, AS, P7, B4, LMNORM; :: thesis: verum

end;

take m ; :: thesis: for n being Nat st m <= n holds
||.((seq . n) - s).|| < r
thus for n being Nat st m <= n holds
||.((seq . n) - s).|| < r by BK; :: thesis: verum

end;

hence seq is convergent ; :: thesis: verum

end;

hence X is RealBanachSpace by LOPBAN_1:def 15; :: thesis: verum