let f be real-valued decreasing FinSequence; :: thesis: min_p f = len f

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

suppose len f = 0 ; :: thesis: min_p f = len f

hence min_p f = len f by RFINSEQ2:def 2; :: thesis: verum

end;

suppose A1: len f > 0 ; :: thesis: min_p f = len f

then len f >= 0 + 1 by NAT_1:13;
then A2: len f in dom f by FINSEQ_3:25;
A3: for i being Nat st i in dom f holds
f . i >= f . (len f)

proof

let i be Nat; :: thesis: ( i in dom f implies f . i >= f . (len f) )
assume A4: i in dom f ; :: thesis: f . i >= f . (len f)
i <= len f by A4, FINSEQ_3:25;

per cases then ( i = len f or i < len f ) by XXREAL_0:1;

suppose i = len f ; :: thesis: f . i >= f . (len f)

hence f . i >= f . (len f) ; :: thesis: verum

end;

suppose i < len f ; :: thesis: f . i >= f . (len f)

hence f . i >= f . (len f) by A2, A4, VALUED_0:def 14; :: thesis: verum

end;

end;

end;

dom f c= REAL by NUMBERS:19;
then f is REAL -defined by RELAT_1:def 18;
then for j being Nat st j in dom f & f . j = f . (len f) holds
len f <= j by A2, FUNCT_1:def 4;
hence min_p f = len f by A1, A2, A3, RFINSEQ2:def 2; :: thesis: verum

end;

end;