let seq be Real_Sequence; :: thesis: ( seq is convergent implies lim (abs seq) = abs (lim seq) )
assume A1: seq is convergent ; :: thesis: lim (abs seq) = abs (lim seq)

now

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((abs seq) . m) - (abs (lim seq))) < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((abs seq) . m) - (abs (lim seq))) < p
then consider n1 being Element of NAT such that
A2: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (lim seq)) < p by A1, SEQ_2:def 7;
take n = n1; :: thesis: for m being Element of NAT st n <= m holds
abs (((abs seq) . m) - (abs (lim seq))) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((abs seq) . m) - (abs (lim seq))) < p )
abs ((lim seq) - (seq . m)) = abs (- ((seq . m) - (lim seq)))
.= abs ((seq . m) - (lim seq)) by COMPLEX1:52 ;
then (abs (lim seq)) - (abs (seq . m)) <= abs ((seq . m) - (lim seq)) by COMPLEX1:59;
then ( (abs (seq . m)) - (abs (lim seq)) <= abs ((seq . m) - (lim seq)) & - (abs ((seq . m) - (lim seq))) <= - ((abs (lim seq)) - (abs (seq . m))) ) by COMPLEX1:59, XREAL_1:24;
then abs ((abs (seq . m)) - (abs (lim seq))) <= abs ((seq . m) - (lim seq)) by ABSVALUE:5;
then A3: abs (((abs seq) . m) - (abs (lim seq))) <= abs ((seq . m) - (lim seq)) by SEQ_1:12;
assume n <= m ; :: thesis: abs (((abs seq) . m) - (abs (lim seq))) < p
then abs ((seq . m) - (lim seq)) < p by A2;
hence abs (((abs seq) . m) - (abs (lim seq))) < p by A3, XXREAL_0:2; :: thesis: verum

end;

hence lim (abs seq) = abs (lim seq) by A1, SEQ_2:def 7; :: thesis: verum