theorem Th15: :: RFINSEQ2:15

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