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 )

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

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

hence
f is convergent
by SEQ_2:def 6; :: thesis: lim f = gex 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;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

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