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

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

suppose A4: len f > 0 ; :: thesis: min f >= min g

dom g = Seg (len g) by FINSEQ_1:def 3;
then A5: dom P = dom g by A3, A4, FUNCT_2:def 1;
A6: min_p f in dom (g * P) by A2, A4, Def2;
then A7: (g * P) . (min_p f) = g . (P . (min_p f)) by FUNCT_1:12;
min_p f in dom g by A1, A2, A6, RFINSEQ:3;
then A8: ( rng P = dom g & P . (min_p f) in rng P ) by A5, FUNCT_1:def 3, FUNCT_2:def 3;
reconsider n = P . (min_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 min f >= min g by A2, A7, Th2; :: thesis: verum

end;

suppose len f <= 0 ; :: thesis: min f >= min g

then ( f = {} & g = {} ) by A3;
hence min f >= min g ; :: thesis: verum

end;

end;