let f be FinSequence of REAL ; :: thesis: for r1, r2 being Real st f = <*r1,r2*> holds
( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 )
let r1, r2 be Real; :: thesis: ( f = <*r1,r2*> implies ( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 ) )
assume A1: f = <*r1,r2*> ; :: thesis: ( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 )
then A2: len f = 2 by FINSEQ_1:61;
then A3: f . 1 >= f . (min_p f) by Th2;
A4: f . 2 = r2 by A1, FINSEQ_1:61;
A5: min_p f in dom f by A2, Def2;
then A6: 1 <= min_p f by FINSEQ_3:27;
A7: f . 2 >= f . (min_p f) by A2, Th2;
A8: f . 1 = r1 by A1, FINSEQ_1:61;
A9: min_p f <= len f by A5, FINSEQ_3:27;

per cases ( r1 <= r2 or r1 > r2 ) ;

suppose r1 <= r2 ; :: thesis: ( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 )

then A10: min r1,r2 >= min f by A8, A3, XXREAL_0:def 9;

now

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

case min_p f < len f ; :: thesis: ( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 )

then min_p f < 1 + 1 by A1, FINSEQ_1:61;
then min_p f <= 1 by NAT_1:13;
then A11: min_p f = 1 by A6, XXREAL_0:1;
then min f >= min r1,r2 by A8, XXREAL_0:17;
then min f = min r1,r2 by A10, XXREAL_0:1;
hence ( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 ) by A8, A11, FUNCOP_1:def 8; :: thesis: verum

end;

case min_p f >= len f ; :: thesis: ( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 )

then A12: min_p f = 2 by A2, A9, XXREAL_0:1;
then min f >= min r1,r2 by A4, XXREAL_0:17;
then A13: min f = min r1,r2 by A10, XXREAL_0:1;
1 in dom f by A2, FINSEQ_3:27;
then r1 <> r2 by A2, A8, A4, A12, Def2;
hence ( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 ) by A4, A12, A13, FUNCOP_1:def 8; :: thesis: verum

end;

end;

end;

hence ( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 ) ; :: thesis: verum

end;

suppose r1 > r2 ; :: thesis: ( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 )

then A14: min r1,r2 >= min f by A4, A7, XXREAL_0:def 9;

now

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

case min_p f < len f ; :: thesis: ( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 )

then min_p f < 1 + 1 by A1, FINSEQ_1:61;
then min_p f <= 1 by NAT_1:13;
then A15: min_p f = 1 by A6, XXREAL_0:1;
then min f >= min r1,r2 by A8, XXREAL_0:17;
then min f = min r1,r2 by A14, XXREAL_0:1;
hence ( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 ) by A8, A15, FUNCOP_1:def 8; :: thesis: verum

end;

case min_p f >= len f ; :: thesis: ( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 )

then A16: min_p f = 2 by A2, A9, XXREAL_0:1;
then min f >= min r1,r2 by A4, XXREAL_0:17;
then A17: min f = min r1,r2 by A14, XXREAL_0:1;
1 in dom f by A2, FINSEQ_3:27;
then r1 <> r2 by A2, A8, A4, A16, Def2;
hence ( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 ) by A4, A16, A17, FUNCOP_1:def 8; :: thesis: verum

end;

end;

end;

hence ( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 ) ; :: thesis: verum

end;

end;