let g be real number ; :: 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

let p be real number ; :: thesis: ( 0 < p implies ex k1 being Element of NAT st
for m being Element of NAT st k1 <= m holds
abs ((f . m) - g) < p )
assume A3: 0 < p ; :: thesis: ex k1 being Element of NAT st
for m being Element of NAT st k1 <= m holds
abs ((f . m) - g) < p
reconsider k1 = k as Element of NAT by ORDINAL1:def 13;
take k1 = k1; :: thesis: for m being Element of NAT st k1 <= m holds
abs ((f . m) - g) < p
thus for m being Element of NAT st k1 <= m holds
abs ((f . m) - g) < p :: thesis: verum

proof

let m be Element of NAT ; :: thesis: ( k1 <= m implies abs ((f . m) - g) < p )
assume k1 <= m ; :: thesis: abs ((f . m) - g) < p
then f . m = g by A1;
hence abs ((f . m) - g) < p by A3, ABSVALUE:7; :: thesis: verum

end;

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