theorem Th10: :: LPSPACE2:10

for seq being Real_Sequence
for n, m being Nat st m <= n holds
( |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= ((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m) & |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= (Partial_Sums (abs seq)) . n )