let n be Nat; :: thesis: REAL-NS n is RealBanachSpace
for seq being sequence of (REAL-NS n) st seq is Cauchy_sequence_by_Norm holds
seq is convergent by Th12;
hence REAL-NS n is RealBanachSpace by LOPBAN_1:def 15; :: thesis: verum