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 ()).| <= Sum (abs ()) )
thus ( <*> REAL = <*> REAL & |.(Sum ()).| <= Sum (abs ()) ) by ; :: 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 ;
take G = p ^ <*x*>; :: thesis: ( G = p ^ <*x*> & |.(Sum G).| <= Sum (abs G) )
A6: abs <*x*> = by JORDAN2B:19;
A7: Sum = |.x.| by RVSUM_1:73;
abs G = (abs p) ^ () by TOPREAL7:11;
then A8: Sum (abs G) = (Sum (abs p)) + |.x.| by ;
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 ; :: thesis: verum
end;
A9: for p being FinSequence of REAL holds S1[p] from f is FinSequence of REAL by RVSUM_1:145;
then S1[f] by A9;
hence |.(Sum f).| <= Sum (abs f) ; :: thesis: verum