let f be real-valued FinSequence; :: thesis: |.(Sum f).| <= Sum (abs f)
defpred S1[ set ] means ex F being real-valued FinSequence st
( F = $1 & |.(Sum F).| <= Sum (abs F) );
A1: S1[ <*> 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 S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of REAL ; :: thesis: for x being Element of REAL st S1[p] holds
S1[p ^ <*x*>]
let x be Element of REAL ; :: thesis: ( S1[p] implies S1[p ^ <*x*>] )
given F being real-valued FinSequence such that A3: F = p and
A4: |.(Sum F).| <= Sum (abs F) ; :: thesis: S1[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 S1[p] from FINSEQ_2:sch 2(A1, A2);
 f is FinSequence of REAL by RVSUM_1:145;
then S1[f] by A9;
hence |.(Sum f).| <= Sum (abs f) ; :: thesis: verum