let f be real-valued FinSequence; :: thesis: abs (- f) = abs f
set n = len f;
reconsider x = f as Element of REAL (len f) by Lm2;

now

let j be Nat; :: thesis: ( j in Seg (len f) implies (abs (- x)) . j = (abs x) . j )
assume j in Seg (len f) ; :: thesis: (abs (- x)) . j = (abs x) . j
reconsider r = f . j, r' = (- f) . j as Element of REAL ;
thus (abs (- x)) . j = abs r' by Th6
.= abs (- r) by RVSUM_1:35
.= abs r by COMPLEX1:138
.= (abs x) . j by Th6 ; :: thesis: verum

end;

hence abs (- f) = abs f by FINSEQ_2:139; :: thesis: verum