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

proof

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

end;

thus g is decreasing :: thesis: verum

proof

let e1, e2 be ExtReal; :: according to VALUED_0:def 14 :: thesis: ( not e1 in proj1 g or not e2 in proj1 g or e2 <= e1 or not g . e1 <= g . e2 )
assume A4: e1 in dom g ; :: thesis: ( not e2 in proj1 g or e2 <= e1 or not g . e1 <= g . e2 )
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 . e1 <= g . e2 )
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 . e1 <= g . e2
then (len f) + k1 < (len f) + k2 by A5, A9, XREAL_1:8;
hence not g . e1 <= g . e2 by A1, A6, A7, A10, A11, VALUED_0:def 14; :: thesis: verum

end;