let f, g be ext-real-valued non-decreasing FinSequence; :: thesis: ( f . (len f) <= g . 1 implies f ^ g is non-decreasing )
assume A1: f . (len f) <= g . 1 ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: (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 A3: ( e1 in dom f & e2 in dom f ) ; :: thesis: (f ^ g) . e1 <= (f ^ g) . e2

then ( (f ^ g) . e1 = f . e1 & (f ^ g) . e2 = f . e2 ) by FINSEQ_1:def 7;
hence (f ^ g) . e1 <= (f ^ g) . e2 by A2, A3, VALUED_0:def 15; :: thesis: verum

end;

suppose A4: ( e1 in dom f & not e2 in dom f ) ; :: thesis: (f ^ g) . e1 <= (f ^ g) . e2

then 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; :: thesis: verum

end;

suppose ( not e1 in dom f & e2 in dom f ) ; :: thesis: (f ^ g) . e1 <= (f ^ g) . e2

then ( ( not 1 <= e1 or not e1 <= len f ) & e2 <= len f & 1 <= e1 ) by A2, FINSEQ_3:25;
hence (f ^ g) . e1 <= (f ^ g) . e2 by XXREAL_0:2, A2; :: thesis: verum

end;

suppose A9: ( not e1 in dom f & not e2 in dom f ) ; :: thesis: (f ^ g) . e1 <= (f ^ g) . e2

then consider i being Nat such that
A10: ( i in dom g & e1 = (len f) + i ) by A2, FINSEQ_1:25;
consider j being Nat such that
A11: ( j in dom g & e2 = (len f) + j ) by A2, FINSEQ_1:25, A9;
( (f ^ g) . e1 = g . i & (f ^ g) . e2 = g . j ) by A10, A11, FINSEQ_1:def 7;
hence (f ^ g) . e1 <= (f ^ g) . e2 by A10, A2, A11, XREAL_1:6, VALUED_0:def 15; :: thesis: verum

end;

end;

end;

hence f ^ g is non-decreasing by VALUED_0:def 15; :: thesis: verum