theorem Th17: :: RINFSUP1:17

for k being Nat
for seq being Real_Sequence st seq is nonnegative holds
seq ^\ k is nonnegative