let n be Nat; :: thesis: for S2 being sequence of (Euclid n) st S2 is Cauchy holds
S2 is convergent
let S2 be sequence of (Euclid n); :: thesis: ( S2 is Cauchy implies S2 is convergent )
assume A1: S2 is Cauchy ; :: thesis: S2 is convergent
reconsider S2NS = S2 as sequence of (REAL-NS n) by Th10;
S2NS is Cauchy_sequence_by_Norm by A1, Th11;
then S2NS is convergent by LOPBAN_1:def 15;
hence S2 is convergent by Th12; :: thesis: verum