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