let f be FinSequence of REAL ; :: thesis: for g being nonnegative-yielding FinSequence of REAL st ( for x being Nat holds f . x >= g . x ) holds
f is nonnegative-yielding
let g be nonnegative-yielding FinSequence of REAL ; :: thesis: ( ( for x being Nat holds f . x >= g . x ) implies f is nonnegative-yielding )
assume A1: for x being Nat holds f . x >= g . x ; :: thesis: f is nonnegative-yielding
for r being Real st r in rng f holds
r >= 0
proof
let r be Real; :: thesis: ( r in rng f implies r >= 0 )
assume B0: r in rng f ; :: thesis: r >= 0
consider k being object such that
B1: ( k in dom f & r = f . k ) by B0, FUNCT_1:def 3;
reconsider k = k as Nat by B1;
g . k >= 0 ;
hence r >= 0 by B1, A1; :: thesis: verum
end;
hence f is nonnegative-yielding by PARTFUN3:def 4; :: thesis: verum