let n be Element of NAT ; :: thesis: REAL-NS n is RealBanachSpace
for seq being sequence of (REAL-NS n) st seq is CCauchy holds
seq is convergent by Th12;
hence REAL-NS n is RealBanachSpace by LOPBAN_1:def 16; :: thesis: verum