let f be real-valued FinSequence; :: thesis: for r being Real st f = <*r*> holds
( min_p f = 1 & min f = r )
let r be Real; :: thesis: ( f = <*r*> implies ( min_p f = 1 & min f = r ) )
assume A1: f = <*r*> ; :: thesis: ( min_p f = 1 & min f = r )
then A2: f . 1 = r ;
A3: len f = 1 by A1, FINSEQ_1:40;
then min_p f in dom f by Def2;
then ( 1 <= min_p f & min_p f <= len f ) by FINSEQ_3:25;
hence ( min_p f = 1 & min f = r ) by A3, A2, XXREAL_0:1; :: thesis: verum