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

now

let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((InvShift r) . m) - 0c ) < p )
assume a2: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((InvShift r) . m) - 0c ) < p
consider k1 being Element of NAT such that
A3: p " < k1 by SEQ_4:10;
take n = k1; :: thesis: for m being Element of NAT st n <= m holds
abs (((InvShift r) . m) - 0c ) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((InvShift r) . m) - 0c ) < p )
assume A4: n <= m ; :: thesis: abs (((InvShift r) . m) - 0c ) < p
(p " ) + 0 < k1 + r by A1, A3, XREAL_1:10;
then A5: 1 / (k1 + r) < 1 / (p " ) by a2, XREAL_1:78;
n + r <= m + r by A4, XREAL_1:8;
then 1 / (m + r) <= 1 / (n + r) by A1, XREAL_1:120;
then A6: 1 / (m + r) < p by A5, XXREAL_0:2;
(InvShift r) . m = 1 / (m + r) by Def2;
hence abs (((InvShift r) . m) - 0c ) < p by A6, ABSVALUE:def 1, A1; :: thesis: verum

end;

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