theorem Th50: :: CATALAN2:50

for Fr being XFinSequence of REAL ex absFr being XFinSequence of REAL st
( dom absFr = dom Fr & |.(Sum Fr).| <= Sum absFr & ( for i being Nat st i in dom absFr holds
absFr . i = |.(Fr . i).| ) )