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 Th30;
then 1 in Seg (len (sort_d f)) by A1, FINSEQ_1:3;
then A3: 1 in dom (sort_d f) by FINSEQ_1:def 3;
A4: for i being Element of 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 Element of 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 A5: ( i in dom (sort_d f) & r1 = (sort_d f) . i & r2 = (sort_d f) . 1 ) ; :: thesis: r1 <= r2
then i in Seg (len (sort_d f)) by FINSEQ_1:def 3;
then A6: 1 <= i by FINSEQ_1:3;
now
per cases ( 1 = i or 1 <> i ) ;
case 1 = i ; :: thesis: r1 <= r2
hence r1 <= r2 by A5; :: thesis: verum
end;
end;
end;
hence r1 <= r2 ; :: thesis: verum
end;
A7: for j being Element of NAT st j in dom (sort_d f) & (sort_d f) . j = (sort_d f) . 1 holds
1 <= j
proof
let j be Element of NAT ; :: thesis: ( j in dom (sort_d f) & (sort_d f) . j = (sort_d f) . 1 implies 1 <= j )
assume ( j in dom (sort_d f) & (sort_d f) . j = (sort_d f) . 1 ) ; :: thesis: 1 <= j
then j in Seg (len (sort_d f)) by FINSEQ_1:def 3;
hence 1 <= j by FINSEQ_1:3; :: thesis: verum
end;
A8: f, sort_d f are_fiberwise_equipotent by Def5;
A9: (sort_d f) . 1 = max (sort_d f) by A1, A2, A3, A4, A7, Def1
.= max f by A8, Th14 ;
A10: len (sort_a f) = len f by Th31;
then A11: 1 in dom (sort_a f) by A1, FINSEQ_3:27;
A12: for i being Element of 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 Element of 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 A13: ( i in dom (sort_a f) & r1 = (sort_a f) . i & r2 = (sort_a f) . 1 ) ; :: thesis: r1 >= r2
then A14: 1 <= i by FINSEQ_3:27;
per cases ( 1 = i or 1 <> i ) ;
suppose 1 = i ; :: thesis: r1 >= r2
hence r1 >= r2 by A13; :: thesis: verum
end;
end;
end;
A15: for j being Element of NAT st j in dom (sort_a f) & (sort_a f) . j = (sort_a f) . 1 holds
1 <= j by FINSEQ_3:27;
A16: f, sort_a f are_fiberwise_equipotent by Def6;
(sort_a f) . 1 = min (sort_a f) by A1, A10, A11, A12, A15, Def2
.= min f by A16, Th15 ;
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, A7, A9, A10, A11, A12, A15, Def1, Def2; :: thesis: verum