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