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;
( (Partial_Sums s) . n <= abs ((Partial_Sums s) . n) & abs ((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