let f be real-valued FinSequence; :: thesis: |.(Sum f).| <= Sum (abs f)
defpred S₁[ set ] means ex F being real-valued FinSequence st
( F = $1 & |.(Sum F).| <= Sum (abs F) );
A1: S₁[ <*> REAL]

proof

take <*> REAL ; :: thesis: ( <*> REAL = <*> REAL & |.(Sum (<*> REAL)).| <= Sum (abs (<*> REAL)) )
thus ( <*> REAL = <*> REAL & |.(Sum (<*> REAL)).| <= Sum (abs (<*> REAL)) ) by ABSVALUE:2, RVSUM_1:72; :: thesis: verum

end;

A2: for p being FinSequence of REAL
for x being Element of REAL st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of REAL ; :: thesis: for x being Element of REAL st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of REAL ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
given F being real-valued FinSequence such that A3: F = p and
A4: |.(Sum F).| <= Sum (abs F) ; :: thesis: S₁[p ^ <*x*>]
A5: |.(Sum F).| + |.x.| <= (Sum (abs F)) + |.x.| by A4, XREAL_1:6;
take G = p ^ <*x*>; :: thesis: ( G = p ^ <*x*> & |.(Sum G).| <= Sum (abs G) )
A6: abs <*x*> = <*|.x.|*> by JORDAN2B:19;
A7: Sum <*|.x.|*> = |.x.| by RVSUM_1:73;
abs G = (abs p) ^ (abs <*x*>) by TOPREAL7:11;
then A8: Sum (abs G) = (Sum (abs p)) + |.x.| by A6, A7, RVSUM_1:75;
Sum G = (Sum p) + x by RVSUM_1:74;
then |.(Sum G).| <= |.(Sum p).| + |.x.| by COMPLEX1:56;
hence ( G = p ^ <*x*> & |.(Sum G).| <= Sum (abs G) ) by A8, A3, A5, XXREAL_0:2; :: thesis: verum

end;

A9: for p being FinSequence of REAL holds S₁[p] from FINSEQ_2:sch 2(A1, A2);
f is FinSequence of REAL by RVSUM_1:145;
then S₁[f] by A9;
hence |.(Sum f).| <= Sum (abs f) ; :: thesis: verum