theorem Th14: :: POLYNOM5:14

for p being FinSequence of the carrier of F_Complex holds |.(Sum p).| <= Sum |.p.|