take s = len p; :: according to ALGSEQ_1:def 1 :: thesis: for b_{1} being set holds

( not s <= b_{1} or (- p) . b_{1} = 0. L )

let i be Nat; :: thesis: ( not s <= i or (- p) . i = 0. L )

assume A1: i >= s ; :: thesis: (- p) . i = 0. L

thus (- p) . i = - (p . i) by BHSP_1:44

.= - (0. L) by A1, ALGSEQ_1:8

.= 0. L by RLVECT_1:12 ; :: thesis: verum

( not s <= b

let i be Nat; :: thesis: ( not s <= i or (- p) . i = 0. L )

assume A1: i >= s ; :: thesis: (- p) . i = 0. L

thus (- p) . i = - (p . i) by BHSP_1:44

.= - (0. L) by A1, ALGSEQ_1:8

.= 0. L by RLVECT_1:12 ; :: thesis: verum