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

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

hence
seq ^\ k is non-zero
by Th7; :: thesis: verumlet 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;(seq ^\ k) . n = seq . (n + k) by NAT_1:def 3;

hence (seq ^\ k) . n <> 0. S by A1, Th7; :: thesis: verum