set Q = Polynom-Ring L;
let x, y be Element of (Polynom-Ring L); :: according to VECTSP_2:def 1 :: thesis: ( not x * y = 0. (Polynom-Ring L) or x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) )
assume aa: x * y = 0. (Polynom-Ring L) ; :: thesis: ( x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) )
assume AS: ( x <> 0. (Polynom-Ring L) & y <> 0. (Polynom-Ring L) ) ; :: thesis: contradiction
reconsider p = x as Polynomial of L by POLYNOM3:def 10;
reconsider q = y as Polynomial of L by POLYNOM3:def 10;
p <> 0_. L by AS, POLYNOM3:def 10;
then reconsider p = p as non zero Polynomial of L by defzer;
q <> 0_. L by AS, POLYNOM3:def 10;
then reconsider q = q as non zero Polynomial of L by defzer;
p <> 0_. L ;
then deg p <> - 1 by HURWITZ:20;
then Ap: len p <> 0 ;
(len p) + 1 > 0 + 1 by Ap, XREAL_1:8;
then Dp: len p >= 1 by NAT_1:13;
then (len p) - 1 >= 1 - 1 by XREAL_1:9;
then Cp: (len p) -' 1 = (len p) - 1 by XREAL_0:def 2;
then reconsider lp = (len p) - 1 as Nat ;
q <> 0_. L ;
then deg q <> - 1 by HURWITZ:20;
then Aq: len q <> 0 ;
(len q) + 1 > 0 + 1 by Aq, XREAL_1:8;
then Dq: len q >= 1 by NAT_1:13;
then Eq: (len q) - 1 >= 1 - 1 by XREAL_1:9;
then (len q) -' 1 = (len q) - 1 by XREAL_0:def 2;
then reconsider lq = (len q) - 1 as Nat ;
set m = ((len p) + (len q)) - 2;
(len p) + (len q) >= 1 + 1 by Dp, Dq, XREAL_1:7;
then ((len p) + (len q)) - 2 >= 2 - 2 by XREAL_1:9;
then reconsider m = ((len p) + (len q)) - 2 as Element of NAT by INT_1:3;
consider r being FinSequence of the carrier of L such that
X: ( len r = m + 1 & (p *' q) . m = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((m + 1) -' k)) ) ) by POLYNOM3:def 9;
((((len p) + (len q)) - 2) + 1) - (len p) = lq ;
then X1a: (m + 1) -' (len p) = lq by XREAL_0:def 2;
X6: (len p) + 0 <= (len p) + ((len q) - 1) by Eq, XREAL_1:6;
then len p in Seg (len r) by Dp, X;
then X1: len p in dom r by FINSEQ_1:def 3;
then X2: r . (len p) = (p . lp) * (q . lq) by X1a, Cp, X;

X4: now :: thesis: for k being Element of NAT st k in dom r & k <> len p holds
r . k = 0. L

let k be Element of NAT ; :: thesis: ( k in dom r & k <> len p implies r . k = 0. L )
assume Y: ( k in dom r & k <> len p ) ; :: thesis: r . k = 0. L

now :: thesis: r . k = 0. L

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

suppose k > len p ; :: thesis: r . k = 0. L

then k >= (len p) + 1 by NAT_1:13;
then H: k - 1 >= ((len p) + 1) - 1 by XREAL_1:9;
k -' 1 >= len p by H, XREAL_0:def 2;
then p . (k -' 1) = 0. L by ALGSEQ_1:8;
then (p . (k -' 1)) * (q . ((m + 1) -' k)) = 0. L by VECTSP_1:7;
hence r . k = 0. L by Y, X; :: thesis: verum

end;

suppose U: k <= len p ; :: thesis: r . k = 0. L

k < len p by Y, U, XXREAL_0:1;
then (m + 1) - k > (m + 1) - (len p) by XREAL_1:10;
then (m + 1) - k >= ((len q) - 1) + 1 by INT_1:7;
then (m + 1) -' k >= len q by XREAL_0:def 2;
then q . ((m + 1) -' k) = 0. L by ALGSEQ_1:8;
then (p . (k -' 1)) * (q . ((m + 1) -' k)) = 0. L by VECTSP_1:6;
hence r . k = 0. L by Y, X; :: thesis: verum

end;

end;

end;

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

end;

X3: now :: thesis: for i being Element of NAT st i in dom r & i <> len p holds
r /. i = 0. L

let i be Element of NAT ; :: thesis: ( i in dom r & i <> len p implies r /. i = 0. L )
assume Y: ( i in dom r & i <> len p ) ; :: thesis: r /. i = 0. L
then i in Seg (len r) by FINSEQ_1:def 3;
then ( 1 <= i & i <= len r ) by FINSEQ_1:1;
hence r /. i = r . i by FINSEQ_4:15
.= 0. L by Y, X4 ;
:: thesis: verum

end;

X5: (p *' q) . m = r /. (len p) by X, X1, X3, POLYNOM2:3
.= (p . lp) * (q . lq) by X2, X6, Dp, X, FINSEQ_4:15 ;
len p = lp + 1 ;
then XX: p . lp <> 0. L by ALGSEQ_1:10;
len q = lq + 1 ;
then q . lq <> 0. L by ALGSEQ_1:10;
then X6: (p *' q) . m <> 0. L by XX, X5, VECTSP_2:def 1;
(0_. L) . m = 0. L by FUNCOP_1:7;
then p *' q <> 0. (Polynom-Ring L) by X6, POLYNOM3:def 10;
hence contradiction by aa, POLYNOM3:def 10; :: thesis: verum