let f be FinSequence of REAL ; :: 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
for r1, r2 being Real st i in dom (sort_d f) & r1 = (sort_d f) . i & r2 = (sort_d f) . 1 holds
r1 <= r2

proof

let i be Nat; :: thesis: for r1, r2 being Real st i in dom (sort_d f) & r1 = (sort_d f) . i & r2 = (sort_d f) . 1 holds
r1 <= r2
let r1, r2 be Real; :: thesis: ( i in dom (sort_d f) & r1 = (sort_d f) . i & r2 = (sort_d f) . 1 implies r1 <= r2 )
assume that
A5: i in dom (sort_d f) and
A6: ( r1 = (sort_d f) . i & r2 = (sort_d f) . 1 ) ; :: thesis: r1 <= r2
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 & r1 <= r2 ) or ( 1 <> i & r1 <= r2 ) )

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

case 1 = i ; :: thesis: r1 <= r2

hence r1 <= r2 by A6; :: thesis: verum

end;

case 1 <> i ; :: thesis: r1 <= r2

then 1 < i by A7, XXREAL_0:1;
hence r1 <= r2 by A3, A5, A6, RFINSEQ:19; :: thesis: verum

end;

end;

end;

hence r1 <= r2 ; :: 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
for r1, r2 being Real st i in dom (sort_a f) & r1 = (sort_a f) . i & r2 = (sort_a f) . 1 holds
r1 >= r2

proof

let i be Nat; :: thesis: for r1, r2 being Real st i in dom (sort_a f) & r1 = (sort_a f) . i & r2 = (sort_a f) . 1 holds
r1 >= r2
let r1, r2 be Real; :: thesis: ( i in dom (sort_a f) & r1 = (sort_a f) . i & r2 = (sort_a f) . 1 implies r1 >= r2 )
assume that
A11: i in dom (sort_a f) and
A12: ( r1 = (sort_a f) . i & r2 = (sort_a f) . 1 ) ; :: thesis: r1 >= r2
A13: 1 <= i by A11, FINSEQ_3:25;

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

suppose 1 = i ; :: thesis: r1 >= r2

hence r1 >= r2 by A12; :: thesis: verum

end;

suppose 1 <> i ; :: thesis: r1 >= r2

then 1 < i by A13, XXREAL_0:1;
hence r1 >= r2 by A9, A11, A12, 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