let f be real-valued FinSequence; :: thesis: ( len f >= 1 implies ( max_p (sort_d f) = 1 & min_p (sort_a f) = 1 & (sort_d f) . 1 = max f & (sort_a f) . 1 = min f ) )
assume A1: len f >= 1 ; :: thesis: ( max_p (sort_d f) = 1 & min_p (sort_a f) = 1 & (sort_d f) . 1 = max f & (sort_a f) . 1 = min f )
A2: len (sort_d f) = len f by Th28;
then 1 in Seg (len (sort_d f)) by A1, FINSEQ_1:1;
then A3: 1 in dom (sort_d f) by FINSEQ_1:def 3;
A4: for i being Nat st i in dom (sort_d f) holds
(sort_d f) . i <= (sort_d f) . 1

proof

let i be Nat; :: thesis: ( i in dom (sort_d f) implies (sort_d f) . i <= (sort_d f) . 1 )
assume A5: i in dom (sort_d f) ; :: thesis: (sort_d f) . i <= (sort_d f) . 1
set r1 = (sort_d f) . i;
set r2 = (sort_d f) . 1;
i in Seg (len (sort_d f)) by A5, FINSEQ_1:def 3;
then A7: 1 <= i by FINSEQ_1:1;

now :: thesis: ( ( 1 = i & (sort_d f) . i <= (sort_d f) . 1 ) or ( 1 <> i & (sort_d f) . i <= (sort_d f) . 1 ) )

per cases ( 1 = i or 1 <> i ) ;

case 1 = i ; :: thesis: (sort_d f) . i <= (sort_d f) . 1

hence (sort_d f) . i <= (sort_d f) . 1 ; :: thesis: verum

end;

case 1 <> i ; :: thesis: (sort_d f) . i <= (sort_d f) . 1

then 1 < i by A7, XXREAL_0:1;
hence (sort_d f) . i <= (sort_d f) . 1 by A3, A5, RFINSEQ:19; :: thesis: verum

end;

end;

end;

hence (sort_d f) . i <= (sort_d f) . 1 ; :: thesis: verum

end;

A8: len (sort_a f) = len f by Th29;
then A9: 1 in dom (sort_a f) by A1, FINSEQ_3:25;
A10: for i being Nat st i in dom (sort_a f) holds
(sort_a f) . i >= (sort_a f) . 1

proof

let i be Nat; :: thesis: ( i in dom (sort_a f) implies (sort_a f) . i >= (sort_a f) . 1 )
assume A11: i in dom (sort_a f) ; :: thesis: (sort_a f) . i >= (sort_a f) . 1
set r1 = (sort_a f) . i;
set r2 = (sort_a f) . 1;
A13: 1 <= i by A11, FINSEQ_3:25;

per cases ( 1 = i or 1 <> i ) ;

suppose 1 = i ; :: thesis: (sort_a f) . i >= (sort_a f) . 1

hence (sort_a f) . i >= (sort_a f) . 1 ; :: thesis: verum

end;

suppose 1 <> i ; :: thesis: (sort_a f) . i >= (sort_a f) . 1

then 1 < i by A13, XXREAL_0:1;
hence (sort_a f) . i >= (sort_a f) . 1 by A9, A11, Th17; :: thesis: verum

end;

end;

end;

A14: f, sort_a f are_fiberwise_equipotent by Def6;
A15: f, sort_d f are_fiberwise_equipotent by Def5;
A16: for j being Nat st j in dom (sort_a f) & (sort_a f) . j = (sort_a f) . 1 holds
1 <= j by FINSEQ_3:25;
then A17: (sort_a f) . 1 = min (sort_a f) by A1, A8, A9, A10, Def2
.= min f by A14, Th15 ;
A18: for j being Nat st j in dom (sort_d f) & (sort_d f) . j = (sort_d f) . 1 holds
1 <= j

proof

let j be Nat; :: thesis: ( j in dom (sort_d f) & (sort_d f) . j = (sort_d f) . 1 implies 1 <= j )
assume that
A19: j in dom (sort_d f) and
(sort_d f) . j = (sort_d f) . 1 ; :: thesis: 1 <= j
j in Seg (len (sort_d f)) by A19, FINSEQ_1:def 3;
hence 1 <= j by FINSEQ_1:1; :: thesis: verum

end;

then (sort_d f) . 1 = max (sort_d f) by A1, A2, A3, A4, Def1
.= max f by A15, Th14 ;
hence ( max_p (sort_d f) = 1 & min_p (sort_a f) = 1 & (sort_d f) . 1 = max f & (sort_a f) . 1 = min f ) by A1, A2, A3, A4, A18, A8, A9, A10, A16, A17, Def1, Def2; :: thesis: verum