set s = InvShift r;
now :: thesis: for n being Element of NAT holds (InvShift r) . n <> 0c
let n be Element of NAT ; :: thesis: (InvShift r) . n <> 0c
1 / (n + r) <> 0 ;
hence (InvShift r) . n <> 0c by Def2; :: thesis: verum
end;
hence InvShift r is non-zero by COMSEQ_1:4; :: thesis: InvShift r is 0 -convergent
lim (InvShift r) = 0 by Th3;
hence InvShift r is 0 -convergent ; :: thesis: verum