let n be Element of 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;
A1: (Partial_Sums s) . n <= abs ((Partial_Sums s) . n) by ABSVALUE:11;
abs ((Partial_Sums s) . n) <= (Partial_Sums (abs s)) . n by Th41;
hence (Partial_Sums s) . n <= (Partial_Sums (abs s)) . n by A1, XXREAL_0:2; :: thesis: verum