let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = 0 iff ( abs seq is convergent & lim (abs seq) = 0 ) )
thus ( seq is convergent & lim seq = 0 implies ( abs seq is convergent & lim (abs seq) = 0 ) ) :: thesis: ( abs seq is convergent & lim (abs seq) = 0 implies ( seq is convergent & lim seq = 0 ) )

proof

assume A1: ( seq is convergent & lim seq = 0 ) ; :: thesis: ( abs seq is convergent & lim (abs seq) = 0 )
then lim (abs seq) = abs 0 by SEQ_4:27
.= 0 by ABSVALUE:7 ;
hence ( abs seq is convergent & lim (abs seq) = 0 ) by A1, SEQ_4:26; :: thesis: verum

end;

thus ( abs seq is convergent & lim (abs seq) = 0 implies ( seq is convergent & lim seq = 0 ) ) by SEQ_4:28; :: thesis: verum