theorem :: NUMBER17:36

for f, g being ext-real-valued FinSequence st f ^ g is non-increasing holds
( f is non-increasing & g is non-increasing )