let f be FinSequence of REAL ; :: thesis: for r being Real st f = <*r*> holds
( max_p f = 1 & max f = r )
let r be Real; :: thesis: ( f = <*r*> implies ( max_p f = 1 & max f = r ) )
assume f = <*r*> ; :: thesis: ( max_p f = 1 & max f = r )
then A1: ( len f = 1 & f . 1 = r ) by FINSEQ_1:57;
then max_p f in dom f by Def1;
then ( 1 <= max_p f & max_p f <= len f ) by FINSEQ_3:27;
hence ( max_p f = 1 & max f = r ) by A1, XXREAL_0:1; :: thesis: verum