reconsider k = k as Element of NAT by ORDINAL1:def 12;

now :: thesis: for n being Element of NAT holds (seq ^\ k) . n <> 0c

let n be Element of NAT ; :: thesis: (seq ^\ k) . n <> 0c
(seq ^\ k) . n = seq . (n + k) by NAT_1:def 3;
hence (seq ^\ k) . n <> 0c by COMSEQ_1:4; :: thesis: verum

end;

hence seq ^\ k is non-zero by COMSEQ_1:4; :: thesis: verum