let x be Real; :: thesis: for seq being Real_Sequence st ( for n being Nat holds seq . n = x ) holds

( seq is convergent & lim seq = x )

let seq be Real_Sequence; :: thesis: ( ( for n being Nat holds seq . n = x ) implies ( seq is convergent & lim seq = x ) )

assume A1: for n being Nat holds seq . n = x ; :: thesis: ( seq is convergent & lim seq = x )

x in REAL by XREAL_0:def 1;

then A2: seq is constant by A1, VALUED_0:def 18;

hence seq is convergent ; :: thesis: lim seq = x

thus lim seq = seq . 0 by A2, SEQ_4:26

.= x by A1 ; :: thesis: verum

( seq is convergent & lim seq = x )

let seq be Real_Sequence; :: thesis: ( ( for n being Nat holds seq . n = x ) implies ( seq is convergent & lim seq = x ) )

assume A1: for n being Nat holds seq . n = x ; :: thesis: ( seq is convergent & lim seq = x )

x in REAL by XREAL_0:def 1;

then A2: seq is constant by A1, VALUED_0:def 18;

hence seq is convergent ; :: thesis: lim seq = x

thus lim seq = seq . 0 by A2, SEQ_4:26

.= x by A1 ; :: thesis: verum