let f, g be ext-real-valued non-decreasing FinSequence; ( f . (len f) <= g . 1 implies f ^ g is non-decreasing )
assume A1:
f . (len f) <= g . 1
; f ^ g is non-decreasing
set fg = f ^ g;
for e1, e2 being ExtReal st e1 in dom (f ^ g) & e2 in dom (f ^ g) & e1 <= e2 holds
(f ^ g) . e1 <= (f ^ g) . e2
proof
let e1,
e2 be
ExtReal;
( e1 in dom (f ^ g) & e2 in dom (f ^ g) & e1 <= e2 implies (f ^ g) . e1 <= (f ^ g) . e2 )
assume A2:
(
e1 in dom (f ^ g) &
e2 in dom (f ^ g) &
e1 <= e2 )
;
(f ^ g) . e1 <= (f ^ g) . e2
per cases
( ( e1 in dom f & e2 in dom f ) or ( e1 in dom f & not e2 in dom f ) or ( not e1 in dom f & e2 in dom f ) or ( not e1 in dom f & not e2 in dom f ) )
;
suppose A4:
(
e1 in dom f & not
e2 in dom f )
;
(f ^ g) . e1 <= (f ^ g) . e2then consider i being
Nat such that A5:
(
i in dom g &
e2 = (len f) + i )
by A2, FINSEQ_1:25;
A6:
( 1
<= e1 &
e1 <= len f & 1
<= i &
i <= len g )
by A4, A5, FINSEQ_3:25;
then
( 1
<= len f & 1
<= len g )
by XXREAL_0:2;
then
(
len f in dom f & 1
in dom g )
by FINSEQ_3:25;
then A7:
(
f . e1 <= f . (len f) &
g . 1
<= g . i )
by VALUED_0:def 15, A4, A5, A6;
then A8:
f . e1 <= g . 1
by A1, XXREAL_0:2;
(
(f ^ g) . e1 = f . e1 &
(f ^ g) . e2 = g . i )
by A5, A4, FINSEQ_1:def 7;
hence
(f ^ g) . e1 <= (f ^ g) . e2
by A8, A7, XXREAL_0:2;
verum end; end;
end;
hence
f ^ g is non-decreasing
by VALUED_0:def 15; verum