let x be real-valued FinSequence; :: thesis: 0 <= Sum (abs x)
|.(Sum x).| <= Sum (abs x) by TOPREALC:21;
hence 0 <= Sum (abs x) ; :: thesis: verum