let f be real-valued FinSequence; :: thesis: |.(Sum f).| <= Sum (abs f)

defpred S_{1}[ set ] means ex F being real-valued FinSequence st

( F = $1 & |.(Sum F).| <= Sum (abs F) );

A1: S_{1}[ <*> REAL]

for x being Element of REAL st S_{1}[p] holds

S_{1}[p ^ <*x*>]
_{1}[p]
from FINSEQ_2:sch 2(A1, A2);

f is FinSequence of REAL by RVSUM_1:145;

then S_{1}[f]
by A9;

hence |.(Sum f).| <= Sum (abs f) ; :: thesis: verum

defpred S

( F = $1 & |.(Sum F).| <= Sum (abs F) );

A1: S

proof

A2:
for p being FinSequence of REAL
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;thus ( <*> REAL = <*> REAL & |.(Sum (<*> REAL)).| <= Sum (abs (<*> REAL)) ) by ABSVALUE:2, RVSUM_1:72; :: thesis: verum

for x being Element of REAL st S

S

proof

A9:
for p being FinSequence of REAL holds S
let p be FinSequence of REAL ; :: thesis: for x being Element of REAL st S_{1}[p] holds

S_{1}[p ^ <*x*>]

let x be Element of REAL ; :: thesis: ( S_{1}[p] implies S_{1}[p ^ <*x*>] )

given F being real-valued FinSequence such that A3: F = p and

A4: |.(Sum F).| <= Sum (abs F) ; :: thesis: S_{1}[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;S

let x be Element of REAL ; :: thesis: ( S

given F being real-valued FinSequence such that A3: F = p and

A4: |.(Sum F).| <= Sum (abs F) ; :: thesis: S

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

f is FinSequence of REAL by RVSUM_1:145;

then S

hence |.(Sum f).| <= Sum (abs f) ; :: thesis: verum