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 that
A1: seq is convergent and
A2: lim seq = 0 ; :: thesis: ( abs seq is convergent & lim (abs seq) = 0 )
lim (abs seq) = |.0.| by A1, A2, SEQ_4:14
.= 0 by ABSVALUE:2 ;
hence ( abs seq is convergent & lim (abs seq) = 0 ) by A1; :: thesis: verum

end;

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