take s = len p; :: according to ALGSEQ_1:def 2 :: thesis: for b₁ being set holds
( not s <= b₁ or (v * p) . b₁ = 0. L )
let i be Nat; :: thesis: ( not s <= i or (v * p) . i = 0. L )
assume A1: i >= s ; :: thesis: (v * p) . i = 0. L
reconsider ii = i as Element of NAT by ORDINAL1:def 13;
thus (v * p) . i = v * (p . ii) by Def3
.= v * (0. L) by A1, ALGSEQ_1:22
.= 0. L by VECTSP_1:36 ; :: thesis: verum