let n be Nat; :: thesis: for s being Real_Sequence holds (Partial_Sums s) . n <= (Partial_Sums (abs s)) . n
let s be Real_Sequence; :: thesis: (Partial_Sums s) . n <= (Partial_Sums (abs s)) . n
set s1 = abs s;
( (Partial_Sums s) . n <= |.((Partial_Sums s) . n).| & |.((Partial_Sums s) . n).| <= (Partial_Sums (abs s)) . n ) by Th41, ABSVALUE:4;
hence (Partial_Sums s) . n <= (Partial_Sums (abs s)) . n by XXREAL_0:2; :: thesis: verum