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 A1: x * y = 0. (Polynom-Ring L) ; :: thesis: ( x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) )
assume A2: ( 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 A2, POLYNOM3:def 10;
then reconsider p = p as non zero Polynomial of L by Def1;
q <> 0_. L by A2, POLYNOM3:def 10;
then reconsider q = q as non zero Polynomial of L by Def1;
p <> 0_. L ;
then deg p <> - 1 by HURWITZ:20;
then A3: len p <> 0 ;
(len p) + 1 > 0 + 1 by A3, XREAL_1:8;
then A4: len p >= 1 by NAT_1:13;
then (len p) - 1 >= 1 - 1 by XREAL_1:9;
then A5: (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 A6: len q <> 0 ;
(len q) + 1 > 0 + 1 by A6, XREAL_1:8;
then A7: len q >= 1 by NAT_1:13;
then A8: (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 A4, A7, 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
A9: ( 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 A10: (m + 1) -' (len p) = lq by XREAL_0:def 2;
A11: (len p) + 0 <= (len p) + ((len q) - 1) by A8, XREAL_1:6;
then len p in Seg (len r) by A4, A9;
then A12: len p in dom r by FINSEQ_1:def 3;
then A13: r . (len p) = (p . lp) * (q . lq) by A10, A5, A9;

A14: 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 A15: ( 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 A16: k - 1 >= ((len p) + 1) - 1 by XREAL_1:9;
k -' 1 >= len p by A16, XREAL_0:def 2;
then p . (k -' 1) = 0. L by ALGSEQ_1:8;
then (p . (k -' 1)) * (q . ((m + 1) -' k)) = 0. L ;
hence r . k = 0. L by A15, A9; :: thesis: verum

end;

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

k < len p by A15, A17, 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 ;
hence r . k = 0. L by A15, A9; :: thesis: verum

end;

end;

end;

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

end;

A18: 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 A19: ( 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 A19, A14 ;
:: thesis: verum

end;

A20: (p *' q) . m = r /. (len p) by A9, A12, A18, POLYNOM2:3
.= (p . lp) * (q . lq) by A13, A11, A4, A9, FINSEQ_4:15 ;
len p = lp + 1 ;
then A21: p . lp <> 0. L by ALGSEQ_1:10;
len q = lq + 1 ;
then q . lq <> 0. L by ALGSEQ_1:10;
then A22: (p *' q) . m <> 0. L by A21, A20, VECTSP_2:def 1;
(0_. L) . m = 0. L by FUNCOP_1:7;
then p *' q <> 0. (Polynom-Ring L) by A22, POLYNOM3:def 10;
hence contradiction by A1, POLYNOM3:def 10; :: thesis: verum