theorem Th14: :: RFINSEQ2:14

for f, g being real-valued FinSequence st f,g are_fiberwise_equipotent holds
max f = max g