let k be Nat; :: thesis: for seq being Real_Sequence st seq is nonnegative holds
seq ^\ k is nonnegative
let seq be Real_Sequence; :: thesis: ( seq is nonnegative implies seq ^\ k is nonnegative )
assume A1: seq is nonnegative ; :: thesis: seq ^\ k is nonnegative
for n being Nat holds (seq ^\ k) . n >= 0

proof

let n be Nat; :: thesis: (seq ^\ k) . n >= 0
(seq ^\ k) . n = seq . (n + k) by NAT_1:def 3;
hence (seq ^\ k) . n >= 0 by A1; :: thesis: verum

end;

hence seq ^\ k is nonnegative ; :: thesis: verum