rng (f /^ j) c= rng f by FINSEQ_5:33;
then for x being Real st x in rng (f /^ j) holds
x >= 0 by PARTFUN3:def 4;
then f /^ j is nonnegative-yielding by PARTFUN3:def 4;
hence not (f /^ j) . i is negative ; :: thesis: verum