let r be Real; :: thesis: ( 0 < r implies lim (InvShift r) = 0 )
set seq = InvShift r;
assume A1: 0 < r ; :: thesis: lim (InvShift r) = 0

now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((InvShift r) . m) - 0c).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((InvShift r) . m) - 0c).| < p )
assume A2: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((InvShift r) . m) - 0c).| < p
consider k1 being Nat such that
A3: p " < k1 by SEQ_4:3;
take n = k1; :: thesis: for m being Nat st n <= m holds
|.(((InvShift r) . m) - 0c).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((InvShift r) . m) - 0c).| < p )
assume n <= m ; :: thesis: |.(((InvShift r) . m) - 0c).| < p
then n + r <= m + r by XREAL_1:6;
then A4: 1 / (m + r) <= 1 / (n + r) by A1, XREAL_1:118;
A5: (InvShift r) . m = 1 / (m + r) by Def2;
(p ") + 0 < k1 + r by A1, A3, XREAL_1:8;
then 1 / (k1 + r) < 1 / (p ") by A2, XREAL_1:76;
then 1 / (m + r) < p by A4, XXREAL_0:2;
hence |.(((InvShift r) . m) - 0c).| < p by A1, A5, ABSVALUE:def 1; :: thesis: verum

end;

hence lim (InvShift r) = 0 by A1, COMSEQ_2:def 6; :: thesis: verum