let f be Real_Sequence; :: thesis: ( f is 0 -convergent implies f is convergent )
assume f is 0 -convergent ; :: thesis: f is convergent
then f is 0 -convergent ;
hence f is convergent by Def1; :: thesis: verum