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