let f, g be real-valued FinSequence; :: thesis: ( f,g are_fiberwise_equipotent implies min f = min g )
assume f,g are_fiberwise_equipotent ; :: thesis: min f = min g
then ( min f >= min g & min g >= min f ) by Lm2;
hence min f = min g by XXREAL_0:1; :: thesis: verum