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 )

i in NAT by ORDINAL1:def 12;

then consider r being FinSequence of the carrier of L such that

A1: len r = i + 1 and

A2: (p *' q) . i = Sum r and

A3: for k being Element of NAT st k in dom r holds

r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by Def9;

assume i >= s ; :: thesis: (p *' q) . i = 0. L

then len p <= i - (len q) by XREAL_1:19;

then A4: - (len p) >= - (i - (len q)) by XREAL_1:24;

( not s <= b

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

i in NAT by ORDINAL1:def 12;

then consider r being FinSequence of the carrier of L such that

A1: len r = i + 1 and

A2: (p *' q) . i = Sum r and

A3: for k being Element of NAT st k in dom r holds

r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by Def9;

assume i >= s ; :: thesis: (p *' q) . i = 0. L

then len p <= i - (len q) by XREAL_1:19;

then A4: - (len p) >= - (i - (len q)) by XREAL_1:24;

now :: thesis: for k being Element of NAT st k in dom r holds

r . k = 0. L

hence
(p *' q) . i = 0. L
by A2, Th1; :: thesis: verumr . k = 0. L

let k be Element of NAT ; :: thesis: ( k in dom r implies r . b_{1} = 0. L )

assume A5: k in dom r ; :: thesis: r . b_{1} = 0. L

then A6: r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A3;

k <= i + 1 by A1, A5, FINSEQ_3:25;

then A7: (i + 1) - k >= 0 by XREAL_1:48;

end;assume A5: k in dom r ; :: thesis: r . b

then A6: r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A3;

k <= i + 1 by A1, A5, FINSEQ_3:25;

then A7: (i + 1) - k >= 0 by XREAL_1:48;

per cases
( k -' 1 < len p or k -' 1 >= len p )
;

end;

suppose
k -' 1 < len p
; :: thesis: r . b_{1} = 0. L

then
k - 1 < len p
by XREAL_0:def 2;

then - (k - 1) > - (len p) by XREAL_1:24;

then 1 - k > (len q) - i by A4, XXREAL_0:2;

then i + (1 - k) > len q by XREAL_1:19;

then (i + 1) -' k >= len q by A7, XREAL_0:def 2;

then q . ((i + 1) -' k) = 0. L by ALGSEQ_1:8;

hence r . k = 0. L by A6; :: thesis: verum

end;then - (k - 1) > - (len p) by XREAL_1:24;

then 1 - k > (len q) - i by A4, XXREAL_0:2;

then i + (1 - k) > len q by XREAL_1:19;

then (i + 1) -' k >= len q by A7, XREAL_0:def 2;

then q . ((i + 1) -' k) = 0. L by ALGSEQ_1:8;

hence r . k = 0. L by A6; :: thesis: verum