for c, s being non empty positive-yielding XFinSequence of REAL ex d being non empty positive-yielding XFinSequence of REAL ex N being Nat st
for x being Nat st N <= x holds
((polynom c) . x) * ((polynom s) . x) <= (polynom d) . x