theorem Th41: :: E_TRANS2:6

for M being Element of F_Real
for F being FinSequence of F_Real st ( for i being Nat st i in dom F holds
|.(F . i).| <= M ) holds
|.(Product F).| <= M |^ (len F)