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 )
assume A1: seq is Cauchy ; :: thesis: seq is convergent
reconsider seq' = seq as sequence of (REAL-NS n) by Th15;
seq' is convergent by A1, 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