let g be Real; :: thesis: for f being Real_Sequence st ex k being Nat st
for n being Nat st k <= n holds
f . n = g holds
( f is convergent & lim f = g )
let f be Real_Sequence; :: thesis: ( ex k being Nat st
for n being Nat st k <= n holds
f . n = g implies ( f is convergent & lim f = g ) )
given k being Nat such that A1: for n being Nat st k <= n holds
f . n = g ; :: thesis: ( f is convergent & lim f = g )

A2: now :: thesis: for p being Real st 0 < p holds
ex k being Nat st
for m being Nat st k <= m holds
|.((f . m) - g).| < p

let p be Real; :: thesis: ( 0 < p implies ex k being Nat st
for m being Nat st k <= m holds
|.((f . m) - g).| < p )
assume A3: 0 < p ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.((f . m) - g).| < p
take k = k; :: thesis: for m being Nat st k <= m holds
|.((f . m) - g).| < p
let m be Nat; :: thesis: ( k <= m implies |.((f . m) - g).| < p )
assume k <= m ; :: thesis: |.((f . m) - g).| < p
then f . m = g by A1;
hence |.((f . m) - g).| < p by A3, ABSVALUE:2; :: thesis: verum

end;

hence f is convergent by SEQ_2:def 6; :: thesis: lim f = g
hence lim f = g by A2, SEQ_2:def 7; :: thesis: verum