theorem Th36: :: NUMBER08:36

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