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

proof

take <*> REAL ; :: thesis: ( <*> REAL = <*> REAL & abs (Sum (<*> REAL )) <= Sum (abs (<*> REAL )) )
thus ( <*> REAL = <*> REAL & abs (Sum (<*> REAL )) <= Sum (abs (<*> REAL )) ) by ABSVALUE:7, RVSUM_1:102; :: 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: abs (Sum F) <= Sum (abs F) ; :: thesis: S₁[p ^ <*x*>]
A5: (abs (Sum F)) + (abs x) <= (Sum (abs F)) + (abs x) by A4, XREAL_1:8;
take G = p ^ <*x*>; :: thesis: ( G = p ^ <*x*> & abs (Sum G) <= Sum (abs G) )
A6: abs <*x*> = <*(abs x)*> by JORDAN2B:23;
A7: Sum <*(abs x)*> = abs x by RVSUM_1:103;
abs G = (abs p) ^ (abs <*x*>) by TOPREAL7:12;
then A8: Sum (abs G) = (Sum (abs p)) + (abs x) by A6, A7, RVSUM_1:105;
Sum G = (Sum p) + x by RVSUM_1:104;
then abs (Sum G) <= (abs (Sum p)) + (abs x) by COMPLEX1:142;
hence ( G = p ^ <*x*> & abs (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 Th19;
then S₁[f] by A9;
hence abs (Sum f) <= Sum (abs f) ; :: thesis: verum