set s = InvShift r;

now

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-empty by COMSEQ_1:4; :: according to CFDIFF_1:def 1 :: thesis: ( InvShift r is convergent & lim (InvShift r) = 0 )
thus ( InvShift r is convergent & lim (InvShift r) = 0 ) by Th3; :: thesis: verum