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
A4: len p <> 0 by A2, POLYNOM4:8;
consider lp1 being Nat such that
A5: len p = lp1 + 1 by A2, NAT_1:6, POLYNOM4:8;
consider lq1 being Nat such that
A6: len q = lq1 + 1 by A3, NAT_1:6, POLYNOM4:8;
reconsider lp1 = lp1, lq1 = lq1 as Element of NAT by ORDINAL1:def 13;
A7: ( p . lp1 <> 0. L & q . lq1 <> 0. L ) by A5, A6, ALGSEQ_1:25;
set lpq = lp1 + lq1;
consider r being FinSequence of L such that
A8: len r = (lp1 + lq1) + 1 and
A9: (p *' q) . (lp1 + lq1) = Sum r and
A10: 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 11;
A11: len p <= (lp1 + 1) + lq1 by A5, NAT_1:12;
0 + 1 <= len p by A4, NAT_1:13;
then A12: len p in dom r by A8, A11, FINSEQ_3:27;
A13: ((lp1 + lq1) + 1) -' (len p) = (lq1 + (lp1 + 1)) -' (len p)
.= lq1 by A5, NAT_D:34 ;

now

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 13;
A16: r . k1 = (p . (k1 -' 1)) * (q . (((lp1 + lq1) + 1) -' k1)) by A10, 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 & 1 <= d ) by FSM_1:1;
A18: ((lp1 + lq1) + 1) -' k = ((lq1 + d) + k) -' k by A5, A17
.= lq1 + d by NAT_D:34 ;
len q <= lq1 + d by A6, A17, XREAL_1:8;
hence r . k = (p . (k -' 1)) * (0. L) by A16, A18, ALGSEQ_1:22
.= 0. L by VECTSP_1:36 ;
:: 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:22
.= 0. L by VECTSP_1:39 ;
:: thesis: verum

end;

end;

end;

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