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 & f . 1 = r1 & f . 2 = r2 ) by FINSEQ_1:61;
then max_p f in dom f by Def1;
then A3: ( 1 <= max_p f & max_p f <= len f ) by FINSEQ_3:27;
A4: ( f . 1 <= f . (max_p f) & f . 1 <= max f ) by A2, Th1;
A5: ( f . 2 <= f . (max_p f) & f . 2 <= max 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 A6: max r1,r2 <= max f by A2, A4, 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:61;
then max_p f <= 1 by NAT_1:13;
then A7: max_p f = 1 by A3, XXREAL_0:1;
then max f <= max r1,r2 by A2, XXREAL_0:25;
then max f = max r1,r2 by A6, XXREAL_0:1;
hence ( max f = max r1,r2 & max_p f = IFEQ r1,(max r1,r2),1,2 ) by A2, A7, 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 A8: max_p f = 2 by A2, A3, XXREAL_0:1;
1 in dom f by A2, FINSEQ_3:27;
then A9: r1 <> r2 by A2, A8, Def1;
max f <= max r1,r2 by A2, A8, XXREAL_0:25;
then max f = max r1,r2 by A6, XXREAL_0:1;
hence ( max f = max r1,r2 & max_p f = IFEQ r1,(max r1,r2),1,2 ) by A2, A8, A9, 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 A10: max r1,r2 <= max f by A2, A5, 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:61;
then max_p f <= 1 by NAT_1:13;
then A11: max_p f = 1 by A3, XXREAL_0:1;
then max f <= max r1,r2 by A2, 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 A2, 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, A3, XXREAL_0:1;
1 in dom f by A2, FINSEQ_3:27;
then A13: r1 <> r2 by A2, A12, Def1;
max f <= max r1,r2 by A2, A12, 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 A2, 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;

end;

end;

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