theorem :: NUMBER17:35

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