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