let f be FinSequence of REAL ; :: thesis: for r1, r2 being Real st f = <*r1,r2*> holds
( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) )
let r1, r2 be Real; :: thesis: ( f = <*r1,r2*> implies ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) )
assume A1: f = <*r1,r2*> ; :: thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) )
then A2: len f = 2 by FINSEQ_1:44;
then A3: f . 2 <= f . (max_p f) by Th1;
A4: f . 1 = r1 by A1, FINSEQ_1:44;
A5: max_p f in dom f by A2, Def1;
then A6: 1 <= max_p f by FINSEQ_3:25;
A7: max_p f <= len f by A5, FINSEQ_3:25;
A8: f . 2 = r2 by A1, FINSEQ_1:44;
A9: f . 1 <= f . (max_p f) by A2, Th1;

now

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

case r1 >= r2 ; :: thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) )

then A10: max (r1,r2) <= max f by A4, A9, XXREAL_0:def 10;

now

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

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

then max_p f < 1 + 1 by A1, FINSEQ_1:44;
then max_p f <= 1 by NAT_1:13;
then A11: max_p f = 1 by A6, XXREAL_0:1;
then max f <= max (r1,r2) by A4, XXREAL_0:25;
then max f = max (r1,r2) by A10, XXREAL_0:1;
hence ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) by A4, A11, FUNCOP_1:def 8; :: thesis: verum

end;

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

then A12: max_p f = 2 by A2, A7, XXREAL_0:1;
then max f <= max (r1,r2) by A8, XXREAL_0:25;
then A13: max f = max (r1,r2) by A10, XXREAL_0:1;
1 in dom f by A2, FINSEQ_3:25;
then r1 <> r2 by A2, A4, A8, A12, Def1;
hence ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) by A8, A12, A13, FUNCOP_1:def 8; :: thesis: verum

end;

end;

end;

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

end;

case r1 < r2 ; :: thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) )

then A14: max (r1,r2) <= max f by A8, A3, XXREAL_0:def 10;

now

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

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

then max_p f < 1 + 1 by A1, FINSEQ_1:44;
then max_p f <= 1 by NAT_1:13;
then A15: max_p f = 1 by A6, XXREAL_0:1;
then max f <= max (r1,r2) by A4, XXREAL_0:25;
then max f = max (r1,r2) by A14, XXREAL_0:1;
hence ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) by A4, A15, FUNCOP_1:def 8; :: thesis: verum

end;

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

then A16: max_p f = 2 by A2, A7, XXREAL_0:1;
then max f <= max (r1,r2) by A8, XXREAL_0:25;
then A17: max f = max (r1,r2) by A14, XXREAL_0:1;
1 in dom f by A2, FINSEQ_3:25;
then r1 <> r2 by A2, A4, A8, A16, Def1;
hence ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) by A8, A16, A17, FUNCOP_1:def 8; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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