let n be Nat; :: thesis: for f, g being natural-valued FinSequence st f is increasing & f | n = g holds
g is increasing
let f, g be natural-valued FinSequence; :: thesis: ( f is increasing & f | n = g implies g is increasing )
assume A1: ( f is increasing & f | n = g ) ; :: thesis: g is increasing
then A2: dom g c= dom f by RELAT_1:60;
for e1, e2 being ExtReal st e1 in dom g & e2 in dom g & e1 < e2 holds
g . e1 < g . e2
proof
let e1, e2 be ExtReal; :: thesis: ( e1 in dom g & e2 in dom g & e1 < e2 implies g . e1 < g . e2 )
assume A3: ( e1 in dom g & e2 in dom g & e1 < e2 ) ; :: thesis: g . e1 < g . e2
then ( e1 in dom f & e2 in dom f & g . e1 = f . e1 & g . e2 = f . e2 ) by A1, A2, FUNCT_1:47;
hence g . e1 < g . e2 by A3, A1, VALUED_0:def 13; :: thesis: verum
end;
hence g is increasing by VALUED_0:def 13; :: thesis: verum