let k be Element of NAT ; :: thesis: for S being RealNormSpace
for seq being sequence of S st seq is non-zero holds
seq ^\ k is non-zero
let S be RealNormSpace; :: thesis: for seq being sequence of S st seq is non-zero holds
seq ^\ k is non-zero
let seq be sequence of S; :: thesis: ( seq is non-zero implies seq ^\ k is non-zero )
assume A1: seq is non-zero ; :: thesis: seq ^\ k is non-zero
now :: thesis: for n being Nat holds (seq ^\ k) . n <> 0. S
let n be Nat; :: thesis: (seq ^\ k) . n <> 0. S
(seq ^\ k) . n = seq . (n + k) by NAT_1:def 3;
hence (seq ^\ k) . n <> 0. S by A1, Th7; :: thesis: verum
end;
hence seq ^\ k is non-zero by Th7; :: thesis: verum