let L be non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for p, q being Polynomial of L holds
( not p *' q = 0_. L or p = 0_. L or q = 0_. L )
let p, q be Polynomial of L; :: thesis: ( not p *' q = 0_. L or p = 0_. L or q = 0_. L )
assume that
A1: p *' q = 0_. L and
A2: p <> 0_. L and
A3: q <> 0_. L ; :: thesis: contradiction
consider lp1 being Nat such that
A4: len p = lp1 + 1 by A2, NAT_1:6, POLYNOM4:5;
len p <> 0 by A2, POLYNOM4:5;
then A5: 0 + 1 <= len p by NAT_1:13;
consider lq1 being Nat such that
A6: len q = lq1 + 1 by A3, NAT_1:6, POLYNOM4:5;
reconsider lp1 = lp1, lq1 = lq1 as Element of NAT by ORDINAL1:def 12;
A7: p . lp1 <> 0. L by A4, ALGSEQ_1:10;
A8: q . lq1 <> 0. L by A6, ALGSEQ_1:10;
set lpq = lp1 + lq1;
consider r being FinSequence of L such that
A9: len r = (lp1 + lq1) + 1 and
A10: (p *' q) . (lp1 + lq1) = Sum r and
A11: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . (((lp1 + lq1) + 1) -' k)) by POLYNOM3:def 9;
A12: ((lp1 + lq1) + 1) -' (len p) = (lq1 + (lp1 + 1)) -' (len p)
.= lq1 by A4, NAT_D:34 ;
len p <= (lp1 + 1) + lq1 by A4, NAT_1:12;
then A13: len p in dom r by A9, A5, FINSEQ_3:25;

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

let k be Nat; :: thesis: ( k in dom r & k <> len p implies r . b₁ = 0. L )
assume that
A14: k in dom r and
A15: k <> len p ; :: thesis: r . b₁ = 0. L
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
A16: r . k1 = (p . (k1 -' 1)) * (q . (((lp1 + lq1) + 1) -' k1)) by A11, A14;

per cases ( k < len p or k > len p ) by A15, XXREAL_0:1;

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

then consider d being Element of NAT such that
A17: len p = k1 + d and
A18: 1 <= d by FINSEQ_4:84;
A19: len q <= lq1 + d by A6, A18, XREAL_1:6;
((lp1 + lq1) + 1) -' k = ((lq1 + d) + k) -' k by A4, A17
.= lq1 + d by NAT_D:34 ;
hence r . k = (p . (k -' 1)) * (0. L) by A16, A19, ALGSEQ_1:8
.= 0. L ;
:: thesis: verum

end;

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

then k >= (len p) + 1 by NAT_1:13;
then k -' 1 >= ((len p) + 1) -' 1 by NAT_D:42;
then k -' 1 >= len p by NAT_D:34;
hence r . k = (0. L) * (q . (((lp1 + lq1) + 1) -' k)) by A16, ALGSEQ_1:8
.= 0. L ;
:: thesis: verum

end;

end;

end;

then Sum r = r . (len p) by A13, MATRIX_3:12
.= (p . ((len p) -' 1)) * (q . (((lp1 + lq1) + 1) -' (len p))) by A11, A13
.= (p . lp1) * (q . lq1) by A4, A12, NAT_D:34 ;
then Sum r <> 0. L by A7, A8, VECTSP_2:def 1;
hence contradiction by A1, A10, FUNCOP_1:7; :: thesis: verum