let X be RealNormSpace; :: thesis: DualSp X is RealBanachSpace

for seq being sequence of (DualSp X) st seq is Cauchy_sequence_by_Norm holds

seq is convergent by Th42;

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

for seq being sequence of (DualSp X) st seq is Cauchy_sequence_by_Norm holds

seq is convergent by Th42;

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