let f, g be FinSequence of REAL ; :: thesis: ( f,g are_fiberwise_equipotent implies min f = min g )
assume A1: f,g are_fiberwise_equipotent ; :: thesis: min f = min g
then A2: min f >= min g by Lm2;
min g >= min f by A1, Lm2;
hence min f = min g by A2, XXREAL_0:1; :: thesis: verum