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

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

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

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

(len p) + (len q) >= len p by NAT_1:11;

then A2: p . i = 0. L by A1, ALGSEQ_1:8, XXREAL_0:2;

A3: (len p) + (len q) >= len q by NAT_1:11;

thus (p + q) . i = (p . i) + (q . i) by NORMSP_1:def 2

.= (0. L) + (0. L) by A1, A2, A3, ALGSEQ_1:8, XXREAL_0:2

.= 0. L by RLVECT_1:def 4 ; :: thesis: verum

( not s <= b

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

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

(len p) + (len q) >= len p by NAT_1:11;

then A2: p . i = 0. L by A1, ALGSEQ_1:8, XXREAL_0:2;

A3: (len p) + (len q) >= len q by NAT_1:11;

thus (p + q) . i = (p . i) + (q . i) by NORMSP_1:def 2

.= (0. L) + (0. L) by A1, A2, A3, ALGSEQ_1:8, XXREAL_0:2

.= 0. L by RLVECT_1:def 4 ; :: thesis: verum