let f, g be FinSequence of REAL ; :: 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:17;
A3: ( len f = len g & dom f = dom g ) by A1, RFINSEQ:16;

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

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

then A5: max_p f in dom (g * P) by A2, Def1;
then A6: (g * P) . (max_p f) = g . (P . (max_p f)) by FUNCT_1:22;
A7: dom g = Seg (len g) by FINSEQ_1:def 3;
A8: 0 + 1 <= len f by A4, NAT_1:13;
A9: rng P = dom g by FUNCT_2:def 3;
dom g = Seg (len g) by FINSEQ_1:def 3;
then dom g <> {} by A3, A8;
then dom P = dom g by FUNCT_2:def 1;
then A10: P . (max_p f) in rng P by A2, A3, A5, FUNCT_1:def 5;
then reconsider n = P . (max_p f) as Element of NAT by A9;
( 1 <= n & n <= len g ) by A7, A9, A10, FINSEQ_1:3;
hence max f <= max g by A2, A6, Th1; :: thesis: verum

end;

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

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

end;

end;