let n be Element of NAT ; :: thesis: REAL-US n is Hilbert
for seq being sequence of (REAL-US n) st seq is Cauchy holds
seq is convergent

proof

let seq be sequence of (REAL-US n); :: thesis: ( seq is Cauchy implies seq is convergent )
reconsider seq9 = seq as sequence of (REAL-NS n) by Th15;
assume seq is Cauchy ; :: thesis: seq is convergent
then seq9 is convergent by Th12, Th18;
hence seq is convergent by Th16; :: thesis: verum

end;

then REAL-US n is complete by BHSP_3:def 6;
hence REAL-US n is Hilbert by BHSP_3:def 7; :: thesis: verum