let f, g be real-valued FinSequence; :: thesis: ( f,g are_fiberwise_equipotent implies max f <= max g )
assume A1: f,g are_fiberwise_equipotent ; :: thesis: max f <= max g
then consider P being Permutation of (dom g) such that
A2: f = g * P by RFINSEQ:4;
A3: dom f = dom g by A1, RFINSEQ:3;
A4: len f = len g by A1, RFINSEQ:3;

per cases ( len f > 0 or len f <= 0 ) ;

suppose A5: len f > 0 ; :: thesis: max f <= max g

then A6: max_p f in dom (g * P) by A2, Def1;
then A7: (g * P) . (max_p f) = g . (P . (max_p f)) by FUNCT_1:12;
dom g = Seg (len g) by FINSEQ_1:def 3;
then dom P = dom g by A4, A5, FUNCT_2:def 1;
then A8: ( rng P = dom g & P . (max_p f) in rng P ) by A2, A3, A6, FUNCT_1:def 3, FUNCT_2:def 3;
reconsider n = P . (max_p f) as Nat ;
dom g = Seg (len g) by FINSEQ_1:def 3;
then ( 1 <= n & n <= len g ) by A8, FINSEQ_1:1;
hence max f <= max g by A2, A7, Th1; :: thesis: verum

end;

suppose len f <= 0 ; :: thesis: max f <= max g

then ( f = {} & g = {} ) by A4;
hence max f <= max g ; :: thesis: verum

end;

end;