set f = seq_a^ (a,b,c);
for r being Real st r in rng (seq_a^ (a,b,c)) holds
r >= 0

proof

let r be Real; :: thesis: ( r in rng (seq_a^ (a,b,c)) implies r >= 0 )
assume r in rng (seq_a^ (a,b,c)) ; :: thesis: r >= 0
then consider n being object such that
A2: ( n in dom (seq_a^ (a,b,c)) & r = (seq_a^ (a,b,c)) . n ) by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A2;
LL1: r = a to_power ((b * n) + c) by ASYMPT_1:def 1, A2;

now :: thesis: ( ( a = 0 & r >= 0 ) or ( 0 < a & r >= 0 ) )

per cases ( a = 0 or 0 < a ) ;

case CA0: a = 0 ; :: thesis: r >= 0

now :: thesis: ( ( (b * n) + c <> 0 & r >= 0 ) or ( (b * n) + c = 0 & r >= 0 ) )

per cases ( (b * n) + c <> 0 or (b * n) + c = 0 ) ;

case (b * n) + c <> 0 ; :: thesis: r >= 0

hence r >= 0 by CA0, LL1, POWER:def 2; :: thesis: verum

end;

case (b * n) + c = 0 ; :: thesis: r >= 0

hence r >= 0 by POWER:24, LL1; :: thesis: verum

end;

end;

end;

hence r >= 0 ; :: thesis: verum

end;

case 0 < a ; :: thesis: r >= 0

hence r >= 0 by LL1, POWER:34; :: thesis: verum

end;

end;

end;

hence r >= 0 ; :: thesis: verum

end;

hence seq_a^ (a,b,c) is nonnegative-yielding ; :: thesis: verum