let f, g be ext-real-valued FinSequence; :: thesis: ( f ^ g is increasing implies ( f is increasing & g is increasing ) )
assume A1: f ^ g is increasing ; :: thesis: ( f is increasing & g is increasing )
A2: dom f c= dom (f ^ g) by FINSEQ_1:26;
thus f is increasing :: thesis: g is increasing

proof

let e1, e2 be ExtReal; :: according to VALUED_0:def 13 :: thesis: ( not e1 in proj1 f or not e2 in proj1 f or e2 <= e1 or not f . e2 <= f . e1 )
assume e1 in dom f ; :: thesis: ( not e2 in proj1 f or e2 <= e1 or not f . e2 <= f . e1 )
then A3: ( e1 in dom (f ^ g) & f . e1 = (f ^ g) . e1 ) by A2, FINSEQ_1:def 7;
assume e2 in dom f ; :: thesis: ( e2 <= e1 or not f . e2 <= f . e1 )
then ( e2 in dom (f ^ g) & f . e2 = (f ^ g) . e2 ) by A2, FINSEQ_1:def 7;
hence ( e2 <= e1 or not f . e2 <= f . e1 ) by A1, A3, VALUED_0:def 13; :: thesis: verum

end;

thus g is increasing :: thesis: verum

proof

let e1, e2 be ExtReal; :: according to VALUED_0:def 13 :: thesis: ( not e1 in proj1 g or not e2 in proj1 g or e2 <= e1 or not g . e2 <= g . e1 )
assume A4: e1 in dom g ; :: thesis: ( not e2 in proj1 g or e2 <= e1 or not g . e2 <= g . e1 )
then consider k1 being Nat such that
A5: e1 = k1 and
A6: (len f) + k1 in dom (f ^ g) by FINSEQ_1:27;
A7: g . e1 = (f ^ g) . ((len f) + k1) by A4, A5, FINSEQ_1:def 7;
assume A8: e2 in dom g ; :: thesis: ( e2 <= e1 or not g . e2 <= g . e1 )
then consider k2 being Nat such that
A9: e2 = k2 and
A10: (len f) + k2 in dom (f ^ g) by FINSEQ_1:27;
A11: g . e2 = (f ^ g) . ((len f) + k2) by A8, A9, FINSEQ_1:def 7;
assume e1 < e2 ; :: thesis: not g . e2 <= g . e1
then (len f) + k1 < (len f) + k2 by A5, A9, XREAL_1:8;
hence not g . e2 <= g . e1 by A1, A6, A7, A10, A11, VALUED_0:def 13; :: thesis: verum

end;