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

proof

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

end;

thus g is non-increasing :: thesis: verum

proof

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

end;