let L be non empty right_complementable add-associative right_zeroed distributive unital associative doubleLoopStr ; :: thesis:
let p, q be Polynomial of L; :: thesis:
assume that
A1: len p > 0 and
A2: len q > 0 ; :: thesis:
A3: len q >= 0 + 1 by A2, NAT_1:13;
then A4: (len q) - 1 >= 0 by XREAL_1:19;
A5: len p >= 0 + 1 by A1, NAT_1:13;
then (len p) - 1 >= 0 by XREAL_1:19;
then A6: (len p) - 1 = (len p) -' 1 by XREAL_0:def 2;
A7: (len p) + (len q) >= 0 + (1 + 1) by A5, A3, XREAL_1:7;
then A8: ((len p) + (len q)) - 1 >= 1 by XREAL_1:19;
then reconsider i1 = ((len p) + (len q)) - 1 as Element of NAT by INT_1:3;
A9: (i1 -' 1) + 1 = i1 by A8, XREAL_1:235;
set LMp = Leading-Monomial p;
set LMq = Leading-Monomial q;
let x be Element of L; :: thesis:
consider F being FinSequence of the carrier of L such that
A10: eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = Sum F and
A11: len F = len ((Leading-Monomial p) *' (Leading-Monomial q)) and
A12: for n being Element of NAT st n in dom F holds
F . n = (((Leading-Monomial p) *' (Leading-Monomial q)) . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2;
consider r being FinSequence of the carrier of L such that
A13: len r = (i1 -' 1) + 1 and
A14: ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) = Sum r and
A15: for k being Element of NAT st k in dom r holds
r . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . (((i1 -' 1) + 1) -' k)) by POLYNOM3:def 9;
(len p) + 0 <= (len p) + ((len q) - 1) by A4, XREAL_1:7;
then len p in Seg (len r) by A5, A9, A13, FINSEQ_1:1;
then A16: len p in dom r by FINSEQ_1:def 3;
((len p) + ((len q) - 1)) - (len p) >= 0 by A3, XREAL_1:19;
then i1 -' (len p) = ((len p) + ((len q) - 1)) - (len p) by XREAL_0:def 2
.= (len q) -' 1 by A4, XREAL_0:def 2 ;
then A17: r . (len p) = ((Leading-Monomial p) . ((len p) -' 1)) * ((Leading-Monomial q) . ((len q) -' 1)) by A9, A15, A16;

now :: thesis:

let i be Element of NAT ; :: thesis:
assume that
A18: i in dom r and
A19: i <> len p ; :: thesis:
i in Seg (len r) by A18, FINSEQ_1:def 3;
then i >= 0 + 1 by FINSEQ_1:1;
then i - 1 >= 0 by XREAL_1:19;
then i -' 1 = i - 1 by XREAL_0:def 2;
then A20: i -' 1 <> (len p) -' 1 by A6, A19;
thus r /. i = r . i by A18, PARTFUN1:def 6
.= ((Leading-Monomial p) . (i -' 1)) * ((Leading-Monomial q) . (((i1 -' 1) + 1) -' i)) by A15, A18
.= (0. L) * ((Leading-Monomial q) . (((i1 -' 1) + 1) -' i)) by A20, Def1
.= 0. L ; :: thesis:

end;

then A21: Sum r = r /. (len p) by A16, POLYNOM2:3
.= ((Leading-Monomial p) . ((len p) -' 1)) * ((Leading-Monomial q) . ((len q) -' 1)) by A16, A17, PARTFUN1:def 6
.= (p . ((len p) -' 1)) * ((Leading-Monomial q) . ((len q) -' 1)) by Def1
.= (p . ((len p) -' 1)) * (q . ((len q) -' 1)) by Def1 ;
A22: (len q) - 1 = (len q) -' 1 by A4, XREAL_0:def 2;

A23: now :: thesis:

let i be Element of NAT ; :: thesis:
assume that
A24: i in dom F and
A25: i <> i1 ; :: thesis:
consider r1 being FinSequence of the carrier of L such that
A26: len r1 = (i -' 1) + 1 and
A27: ((Leading-Monomial p) *' (Leading-Monomial q)) . (i -' 1) = Sum r1 and
A28: for k being Element of NAT st k in dom r1 holds
r1 . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . (((i -' 1) + 1) -' k)) by POLYNOM3:def 9;
i in Seg (len F) by A24, FINSEQ_1:def 3;
then i >= 1 by FINSEQ_1:1;
then A29: (i -' 1) + 1 = i by XREAL_1:235;

A30: now :: thesis:

let j be Element of NAT ; :: thesis:
assume A31: j in dom r1 ; :: thesis:
then j in Seg (len r1) by FINSEQ_1:def 3;
then j >= 0 + 1 by FINSEQ_1:1;
then j - 1 >= 0 by XREAL_1:19;
then A32: j -' 1 = j - 1 by XREAL_0:def 2;

per cases ;

suppose j <> len p ; :: thesis:

then A33: j -' 1 <> (len p) -' 1 by A6, A32;
thus r1 . j = ((Leading-Monomial p) . (j -' 1)) * ((Leading-Monomial q) . (((i -' 1) + 1) -' j)) by A28, A31
.= (0. L) * ((Leading-Monomial q) . (((i -' 1) + 1) -' j)) by A33, Def1
.= 0. L ; :: thesis:

end;

suppose A34: j = len p ; :: thesis:

j in Seg (len r1) by A31, FINSEQ_1:def 3;
then i >= 0 + j by A26, A29, FINSEQ_1:1;
then i - j >= 0 by XREAL_1:19;
then i -' (len p) = i - (len p) by A34, XREAL_0:def 2;
then A35: i -' (len p) <> (len q) -' 1 by A22, A25;
thus r1 . j = ((Leading-Monomial p) . (j -' 1)) * ((Leading-Monomial q) . (i -' (len p))) by A28, A29, A31, A34
.= ((Leading-Monomial p) . (j -' 1)) * (0. L) by A35, Def1
.= 0. L ; :: thesis:

end;

thus F /. i = F . i by A24, PARTFUN1:def 6
.= (Sum r1) * ((power L) . (x,(i -' 1))) by A12, A24, A27
.= (0. L) * ((power L) . (x,(i -' 1))) by A30, POLYNOM3:1
.= 0. L ; :: thesis:

end;

A36: ((len p) + (len q)) - 2 >= 0 by A7, XREAL_1:19;
((len p) + (len q)) - (1 + 1) >= 0 by A7, XREAL_1:19;
then A37: i1 -' 1 = (((len p) + (len q)) - 1) - 1 by XREAL_0:def 2
.= ((len p) + (len q)) -' 2 by A36, XREAL_0:def 2 ;

per cases ) *' (Leading-Monomial q)) . (i1 -' 1) <> 0. L or ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) = 0. L ) ;

suppose ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) <> 0. L ; :: thesis:

then len F > i1 -' 1 by A11, ALGSEQ_1:8;
then len F >= i1 by A9, NAT_1:13;
then i1 in Seg (len F) by A8, FINSEQ_1:1;
then A38: i1 in dom F by FINSEQ_1:def 3;
hence eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = F /. i1 by A10, A23, POLYNOM2:3
.= F . i1 by A38, PARTFUN1:def 6
.= ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2))) by A12, A14, A37, A21, A38 ;
:: thesis:

end;

suppose A39: ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) = 0. L ; :: thesis:

now :: thesis:

let j be Nat; :: thesis:
assume j >= 0 ; :: thesis:
j in NAT by ORDINAL1:def 12;
then consider r1 being FinSequence of the carrier of L such that
A40: len r1 = j + 1 and
A41: ((Leading-Monomial p) *' (Leading-Monomial q)) . j = Sum r1 and
A42: for k being Element of NAT st k in dom r1 holds
r1 . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . ((j + 1) -' k)) by POLYNOM3:def 9;

now :: thesis:

per cases ;

suppose j = i1 -' 1 ; :: thesis:

hence ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L by A39; :: thesis:

end;

suppose A43: j <> i1 -' 1 ; :: thesis:

now :: thesis:

let k be Element of NAT ; :: thesis:
assume A44: k in dom r1 ; :: thesis:

per cases ;

suppose A45: k -' 1 <> (len p) -' 1 ; :: thesis:

thus r1 . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . ((j + 1) -' k)) by A42, A44
.= (0. L) * ((Leading-Monomial q) . ((j + 1) -' k)) by A45, Def1
.= 0. L ; :: thesis:

end;

suppose A46: k -' 1 = (len p) -' 1 ; :: thesis:

A47: k in Seg (len r1) by A44, FINSEQ_1:def 3;
then 0 + 1 <= k by FINSEQ_1:1;
then k - 1 >= 0 by XREAL_1:19;
then A48: k -' 1 = k - 1 by XREAL_0:def 2;
0 + k <= j + 1 by A40, A47, FINSEQ_1:1;
then (j + 1) - k >= 0 by XREAL_1:19;
then A49: (j + 1) -' k = (j - (len p)) + 1 by A6, A46, A48, XREAL_0:def 2;
A50: (j - (len p)) + 1 <> ((i1 -' 1) - (len p)) + 1 by A43;
thus r1 . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . ((j + 1) -' k)) by A42, A44
.= ((Leading-Monomial p) . (k -' 1)) * (0. L) by A22, A9, A49, A50, Def1
.= 0. L ; :: thesis:

end;

hence ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L by A41, POLYNOM3:1; :: thesis:

end;

hence ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L ; :: thesis:

end;

then 0 is_at_least_length_of (Leading-Monomial p) *' (Leading-Monomial q) ;
then len ((Leading-Monomial p) *' (Leading-Monomial q)) = 0 by ALGSEQ_1:def 3;
then (Leading-Monomial p) *' (Leading-Monomial q) = 0_. L by Th5;
then eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = 0. L by Th17;
hence eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2))) by A14, A21, A39; :: thesis:

end;