let f be real-valued FinSequence; :: 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:44;
then A3: f . 1 >= f . (min_p f) by Th2;
A4: f . 2 = r2 by A1;
A5: min_p f in dom f by A2, Def2;
then A6: 1 <= min_p f by FINSEQ_3:25;
A7: f . 2 >= f . (min_p f) by A2, Th2;
A8: f . 1 = r1 by A1;
A9: min_p f <= len f by A5, FINSEQ_3:25;

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 :: thesis: ( ( min_p f < len f & min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) or ( min_p f >= len f & min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) )

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:44;
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:25;
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 :: thesis: ( ( min_p f < len f & min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) or ( min_p f >= len f & min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) )

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:44;
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:25;
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;